compAddMonoidHom — Mathlib

English

If f is injective, then ψ ↦ f.compAddChar ψ is injective on AddChar B M.

Русский

Если f инъективен, то отображение ψ ↦ f.compAddChar ψ инъективно в AddChar B M.

LaTeX

$$$$ \text{If } f: M \to_* N \text{ is injective, then } \psi \mapsto f \circ \psi \text{ is injective. } $$$$

Lean4

/-- Composing an `AddChar` with an `AddMonoidHom` yields another `AddChar`. -/
def compAddMonoidHom (φ : AddChar B M) (f : A →+ B) : AddChar A M :=
  toAddMonoidHomEquiv.symm (φ.toAddMonoidHom.comp f)

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