quotientInfToPiQuotient_inj — Mathlib

English

Injectivity of quotientInfToPiQuotient, equivalently ker is trivial.

Русский

Инъективность quotientInfToPiQuotient; эквивалентно тривиальности ядра.

LaTeX

$$$\text{Injective}(\operatorname{quotientInfToPiQuotient} I)$$$

Lean4

theorem quotientInfToPiQuotient_inj (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] : Injective (quotientInfToPiQuotient I) :=
  by rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]

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