ringHomComp_inv — Mathlib

English

Post-composition commutes with taking powers: (χ.ringHomComp f)^n = (χ^n).ringHomComp f.

Русский

Композиция после гомоморфизма сохраняет степени: (χ.ringHomComp f)^n = (χ^n).ringHomComp f.

LaTeX

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

Lean4

theorem ringHomComp_inv {R : Type*} [CommMonoidWithZero R] (χ : MulChar R R') (f : R' →+* R'') :
    (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f := by
  ext1
  simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]

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