instIsReflexiveOfFiniteOfProjective

English

If V is finite and projective over R, then V is IsReflexive.

Русский

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

LaTeX

$$[Module.Finite R N] ∧ [Module.Projective R N] ⇒ IsReflexive R N$$

Lean4

instance (priority := 900) [Module.Finite R N] [Projective R N] : IsReflexive R N :=
  have ⟨_, f, hf⟩ := Finite.exists_fin' R N
  have ⟨g, H⟩ := projective_lifting_property f .id hf
  .of_split g f H

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