instLinearEquivClassDual — Mathlib

English

The PerfectPairing induces a LinearEquivClass from PerfectPairing R M N to Linear maps M → Dual R N and back, encoding the duality universally across modules.

Русский

Идеальная пара порождает класс линейных эквивалентов, кодирующий дуальность между M и N в едином виде.

LaTeX

$$$\text{instLinearEquivClassDual}: \text{LinearEquivClass } ( \text{PerfectPairing } R M N ) R M (Dual(R,N))$.$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
instance : LinearEquivClass (PerfectPairing R M N) R M (Dual R N)
    where
  map_add p m₁ m₂ := p.toLinearMap.map_add m₁ m₂
  map_smulₛₗ p t m := p.toLinearMap.map_smul t m

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