quotientInfEquivSupQuotient_injective

English

The canonical map quotientInfToSupQuotient is injective.

Русский

Каноническое отображение quotientInfToSupQuotient инъективно.

LaTeX

$$Function.Injective (quotientInfToSupQuotient p p')$$

Lean4

theorem quotientInfEquivSupQuotient_injective (p p' : Submodule R M) :
    Function.Injective (quotientInfToSupQuotient p p') :=
  by
  rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
  rw [ker_comp, ker_mkQ]
  exact fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩

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