English
Let f: M0 → M be multiplicative with respect to x, i.e., f(xy) = f(x) f(y) for all y. Then for any n ∈ ℕ, f(x^n y) = f(x)^n f(y) for all y.
Русский
Пусть f: M0 → M является гомоморфизмом с сохранением умножения на x, то есть f(xy) = f(x) f(y) для всех y. Тогда для любого n ∈ ℕ выполняется f(x^n y) = f(x)^n f(y) для всех y.
LaTeX
$$$\forall f: M_0 \to M,\ \forall x \in M_0,\ (\forall y \in M_0,\ f(xy)=f(x)f(y)) \Rightarrow \forall n \in \mathbb{N},\ \forall y \in M_0,\ f(x^n y)=f(x)^n f(y)$$$
Lean4
/-- If `x` is multiplicative with respect to `f`, then so is any `x^n`. -/
theorem pow_mul_apply_eq_pow_mul {M : Type*} [Monoid M] (f : M₀ → M) {x : M₀} (hx : ∀ y : M₀, f (x * y) = f x * f y)
(n : ℕ) : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y := by
induction n with
| zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
| succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]
