to_quotient_square_comp_toCotangent

English

The composition I.cotangentToQuotientSquare ∘ I.toCotangent equals (I^2).mkQ ∘ Submodule.subtype I.

Русский

Композицiя I.cotangentToQuotientSquare от I.toCotangent равна (I^2).mkQ ∘ Submodule.subtype I.

LaTeX

$$$I.cotangentToQuotientSquare \\circ I.toCotangent = (I^2).mkQ \\circ \\mathrm{Submodule.subtype}\\,I$$

Lean4

theorem to_quotient_square_comp_toCotangent :
    I.cotangentToQuotientSquare.comp I.toCotangent = (I ^ 2).mkQ.comp (Submodule.subtype I) :=
  LinearMap.ext fun _ => rfl

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