ringHomComp_pow — Mathlib

English

Power compatibility with ringHomComp: χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f.

Русский

Совместимость степеней с ringHomComp: χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f.

LaTeX

$$$$ (\\chi.ringHomComp f)^n = (\\chi^n).ringHomComp f. $$$$

Lean4

theorem ringHomComp_pow (χ : MulChar R R') (f : R' →+* R'') (n : ℕ) : χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f := by
  induction n with
  | zero => simp only [pow_zero, ringHomComp_one]
  | succ n ih => simp only [pow_succ, ih, ringHomComp_mul]

Похожие утверждения