injective_iff — Mathlib

English

Let ψ : AddChar A M. Then ψ is injective if and only if for every x ∈ A, ψ(x) = 1 implies x = 0.

Русский

Пусть ψ: AddChar A M. Тогда ψ инъектива тогда и только тогда, когда для каждого x ∈ A выполняется ψ(x) = 1 → x = 0.

LaTeX

$$$\operatorname{Injective}(\psi) \iff \forall x, \psi(x) = 1 \rightarrow x = 0$$$

Lean4

theorem injective_iff {ψ : AddChar A M} : Injective ψ ↔ ∀ ⦃x⦄, ψ x = 1 → x = 0 :=
  ψ.toMonoidHom.ker_eq_bot_iff.symm.trans eq_bot_iff

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