English
Canonical equality between the coercion of quotientInfToSupQuotient and quotientInfEquivSupQuotient.
Русский
Каноническое соответствие между коэф. quotientInfToSupQuotient и quotientInfEquivSupQuotient.
LaTeX
$$theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) : ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p'$$
Lean4
/-- Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism.
Note that in the following declaration the type of the domain is expressed using
``comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`). -/
noncomputable def quotientInfEquivSupQuotient (p p' : Submodule R M) :
(p ⧸ comap p.subtype p ⊓ comap p.subtype p') ≃ₗ[R] _ ⧸ comap (p ⊔ p').subtype p' :=
LinearEquiv.ofBijective (quotientInfToSupQuotient p p')
⟨quotientInfEquivSupQuotient_injective p p', quotientInfEquivSupQuotient_surjective p p'⟩
