ker_eq_bot_of_cancel — Mathlib

English

Let f: A →* B be a monoid homomorphism. If for all u,v: f.ker →* A we have f ∘ u = f ∘ v implies u = v, then ker f = ⊥ (the kernel is trivial).

Русский

Пусть f: A →* B — гомоморфизм моноида. Если для любых u,v: f.ker →* A выполняется f ∘ u = f ∘ v ⇒ u = v, то ker f = ⊥ (ядро тривиально).

LaTeX

$$$ \ker f = \{e\} \quad\text{если}\quad ∀ u,v:\; f \circ u = f \circ v \Rightarrow u = v $$$

Lean4

@[to_additive]
theorem ker_eq_bot_of_cancel {f : A →* B} (h : ∀ u v : f.ker →* A, f.comp u = f.comp v → u = v) : f.ker = ⊥ := by
  simpa using congr_arg range (h f.ker.subtype 1 (by cat_disch))

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