ringHomComp_one — Mathlib

English

The inverse of a post-composed character equals the post-composition of the inverse: (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f.

Русский

Обратный к χ.ringHomComp f равен χ⁻¹.ringHomComp f.

LaTeX

$$$$ (\\chi.ringHomComp f)^{-1} = \\chi^{-1}.ringHomComp f. $$$$

Lean4

@[simp]
theorem ringHomComp_one (f : R' →+* R'') : (1 : MulChar R R').ringHomComp f = 1 :=
  by
  ext1
  simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]

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