isReflexive_of_equiv_dual_of_isReflexive

English

The instance assigns a perfect pairing structure to the flipped modules, ensuring the dual bijections work coherently under flip.

Русский

Инстанс задаёт структуру совершенной пары для развёрнутых модулей, обеспечивая согласованность биективностей дуальности под flip.

LaTeX

$$$\\text{IsPerfPair}$ for $p.flip$ on swapped modules.$$

Lean4

/-- If `N` is in perfect pairing with `M`, then it is reflexive. -/
theorem isReflexive_of_equiv_dual_of_isReflexive : IsReflexive R N :=
  by
  constructor
  rw [← trans_dualMap_symm_flip e]
  exact LinearEquiv.bijective _

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