coe_associatedHom — Mathlib

English

The linearization of the associated construction agrees with the explicitly defined associated map.

Русский

Линейная конструкция ассоциации совпадает с явно заданным отображением ассоциированного квадратичного отображения.

LaTeX

$$$\\mathrm{coerce}(\\mathrm{associatedHom}(S)) = \\mathrm{coerce}(\\mathrm{associated}).$$$

Lean4

theorem coe_associatedHom : ⇑(associatedHom S : QuadraticMap R M N →ₗ[S] BilinMap R M N) = associated :=
  rfl

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