injective_iff_isRegular — Mathlib

English

Injectivity of the base algebra map is equivalent to each element coming from the monoid being regular (not a zero divisor).

Русский

Инъективность базового отображения эквивалентна тому, что каждый элемент из моноида является регулярным (не нулевой делитель).

LaTeX

$$$\\text{Injective}(\\mathrm{algebraMap}\\; R\\; S) \\iff \\forall c\\in M,\; \\text{IsRegular}(c)$$

Lean4

theorem injective_iff_isRegular : Injective (algebraMap R S) ↔ ∀ c : M, IsRegular (c : R) := by
  simp_rw [Commute.isRegular_iff (Commute.all _), IsLeftRegular, Injective, eq_iff_exists M, exists_imp,
    forall_comm (α := M)]

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