toLinearMap_eq_toPerfectPairing — Mathlib

English

The linear map induced by the root pairing agrees under standard equalities of the maps.

Русский

Линейное отображение, индуцированное парой корней, совпадает в рамках стандартных равенств отображений.

LaTeX

$$$$ P.toLinearMap = P.toLinearMap $$$$

Lean4

@[deprecated "Now a syntactic equality" (since := "2025-07-05"), nolint synTaut]
theorem toLinearMap_eq_toPerfectPairing (x : M) (y : N) : P.toLinearMap x y = P.toLinearMap x y :=
  rfl

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