instIsReflecive — Mathlib

English

If M is a reflexive module over R, then its dual module Dual(R,M) is also reflexive.

Русский

Если M — рефлексивный модуль над R, то двойственный модуль Dual(R,M) тоже рефлексивен.

LaTeX

$$IsReflexive(R,M) \\Rightarrow IsReflexive(R, Dual(R,M)).$$

Lean4

/-- The dual of a reflexive module is reflexive. -/
instance instIsReflecive : IsReflexive R (Dual R M) :=
  ⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩

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