isRegular_of_smul_left_injective — Mathlib

English

If there exists m ∈ M' such that r ↦ r•m is injective, then s ∈ S is regular in R (i.e., multiplication by s is injective).

Русский

Если существует m ∈ M' такая, что r ↦ r•m инъективно, то s ∈ S является регулярным в R (умножение на s инъективно).

LaTeX

$$$\\big(\\exists m \\in M' ,\\ \\operatorname{Injective}(\\lambda r:\\, R\\mapsto r\\cdot m)\\big) \\Rightarrow \\operatorname{IsRegular}(s).$$$

Lean4

theorem isRegular_of_smul_left_injective {m : M'} (inj : Function.Injective fun r : R ↦ r • m) (s : S) :
    IsRegular (s : R) :=
  (Commute.isRegular_iff (Commute.all _)).mpr fun r r' eq ↦
    by
    have := congr_arg (· • m) eq
    simp_rw [mul_smul, ← Submonoid.smul_def, smul_inj f] at this
    exact inj this

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