one_comp — Mathlib

English

Same principle as above: the identity after composition with f yields the identity on the domain.

Русский

Та же идея: после композиции с f единичный отображение даёт единичное отображение на области.

LaTeX

$$$(1 : N \to*₀ G) \circ f = (1 : M \to*₀ G)$$$

Lean4

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

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