of_finite_of_free — Mathlib

English

If R is a ring and M is finite and free, then M is IsReflexive.

Русский

Если модуль M над R конечен и свободен, то он рефлексивен.

LaTeX

$$[Finite R M] ∧ [Free R M] ⇒ IsReflexive R M$$

Lean4

/-- See also `Module.instFiniteDimensionalOfIsReflexive` for the converse over a field. -/
instance (priority := 900) of_finite_of_free [Module.Finite R M] [Free R M] : IsReflexive R M
    where
  bijective_dual_eval'.left := (Free.chooseBasis R M).eval_injective
  bijective_dual_eval'.right := range_eq_top.mp (Free.chooseBasis R M).eval_range

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