quotientQuotientEquivQuotientAux_mk

English

The third isomorphism theorem map between M/S, T/S and M/T exists as a linear map.

Русский

Существование линейного отображения между M/S, T/S и M/T по теореме третьего изоморфизма.

LaTeX

$$(S T : Submodule R M) -> (S ⊆ T) → LinearMap (RingHom.id R) (HasQuotient.Quotient M S) (HasQuotient.Quotient M T)$$

Lean4

@[simp]
theorem quotientQuotientEquivQuotientAux_mk (x : M ⧸ S) :
    quotientQuotientEquivQuotientAux S T h (Quotient.mk x) = mapQ S T LinearMap.id h x :=
  liftQ_apply _ _
    _
      -- @[simp] /- adaption note for https://github.com/leanprover/lean4/pull/8419: the simpNF complained -/

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