English
Let R be a monoid and M an additive monoid with compatible actions, and let x be an element of the trivial square-zero extension tsze.R M. Then for every natural number n, the first component of x raised to the n-th power equals the n-th power of the first component of x; i.e. fst(x^n) = fst(x)^n.
Русский
Пусть R — моноид, M — дополнительно моноид с совместимыми действиями, и пусть x ∈ tsze.R M. Тогда для любого натурального числа n первая координата x^n равна n-й степени первой координаты x; то есть fst(x^n) = fst(x)^n.
LaTeX
$$$\\\\operatorname{fst}(x^n) = (\\\\operatorname{fst} x)^n$$$
Lean4
@[simp]
theorem fst_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ) :
fst (x ^ n) = x.fst ^ n :=
rfl
