apply_one_apply_eq — Mathlib

English

The trivial group-with-zero hom is absorbing for composition: f ∘ 1 = 1 for any f.

Русский

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

LaTeX

$$$f \circ 1 = 1 \quad\text{for all } f : N_{0} \to_{0} G_{0}$$$

Lean4

/-- The trivial group-with-zero hom is absorbing for composition. -/
@[simp]
theorem apply_one_apply_eq {M₀ N₀ G₀ : Type*} [MulZeroOneClass M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
    [MulZeroOneClass N₀] [MulZeroOneClass G₀] [DecidablePred fun x : M₀ ↦ x = 0] (f : N₀ →*₀ G₀) (x : M₀) :
    f ((1 : M₀ →*₀ N₀) x) = (1 : M₀ →*₀ G₀) x :=
  by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  · rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]

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