ringHomComp — Mathlib

English

The identity post-composed by any ring homomorphism remains the identity: (1 : MulChar R R').ringHomComp f = 1.

Русский

Единственный характер после композиции с кольцевым гомоморфизмом остаётся тождественным: (1 : MulChar R R').ringHomComp f = 1.

LaTeX

$$$$ (1 : \\mathrm{MulChar}(R,R')).\\!ringHomComp f = 1. $$$$

Lean4

/-- We can post-compose a multiplicative character with a ring homomorphism. -/
@[simps]
def ringHomComp (χ : MulChar R R') (f : R' →+* R'') : MulChar R R'' :=
  { f.toMonoidHom.comp χ.toMonoidHom with
    toFun := fun a => f (χ a)
    map_nonunit' := fun a ha => by simp only [map_nonunit χ ha, map_zero] }

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