inverse — Mathlib

English

The inverse of a LinearPMap is defined by swapping the roles of E and F via a linear equivalence on the product space.

Русский

Обратное LinearPMap определяется перераспределением ролей E и F через линейное эквивалентное отображение на произведение.

LaTeX

$$inverse : (E →ₗ.[R] F) → (F →ₗ.[R] E)$$

Lean4

/-- The inverse of a `LinearPMap`. -/
noncomputable def inverse (f : E →ₗ.[R] F) : F →ₗ.[R] E :=
  (f.graph.map (LinearEquiv.prodComm R E F)).toLinearPMap

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