comp_one — Mathlib

English

Same as above: the trivial group-with-zero hom is absorbing for composition.

Русский

То же самое: тривиальный гомоморфизм поглощает композицию.

LaTeX

$$$f \circ 1 = 1$$$

Lean4

/-- The trivial group-with-zero hom is absorbing for composition. -/
@[simp]
theorem comp_one {M₀ N₀ G₀ : Type*} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀] [MulZeroOneClass N₀]
    [MulZeroOneClass G₀] [DecidablePred fun x : M₀ ↦ x = 0] (f : N₀ →*₀ G₀) :
    f.comp (1 : M₀ →*₀ N₀) = (1 : M₀ →*₀ G₀) :=
  ext <| apply_one_apply_eq _

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