quotientInfEquivSupQuotient_symm_apply_right

English

For p and p', the symm map sends mk x to the quotient-by-p side.

Русский

Для p и p' симметричное отображение отправляет mk x в соответствующий элемент правой стороны.

LaTeX

$$theorem quotientInfEquivSupQuotient_symm_apply_left (p p' : Submodule R M) (x : Subtype fun x => SetLike.instMembership.mem (SemilatticeSup.toMax.max p p') x) (hx : (x : M) ∈ p) : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨x, hx⟩$$

Lean4

theorem quotientInfEquivSupQuotient_symm_apply_right (p p' : Submodule R M) {x : ↥(p ⊔ p')} (hx : (x : M) ∈ p') :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 :=
  quotientInfEquivSupQuotient_symm_apply_eq_zero_iff.2 hx

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