Theorems · Inductive type · linear algebra
Module.IsReflexive
(R : Type u_3) → (M : Type u_4) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
A reflexive module is one for which the natural map to its double dual is a bijection.
Any finitely-generated projective module (and thus any finite-dimensional vector space)
is reflexive. See Module.instIsReflexiveOfFiniteOfProjective.
- Defined in
- Mathlib.LinearAlgebra.Dual.Defs
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement · cited by 20,661
- AddCommMonoidstatement · cited by 12,281
- CommSemiringstatement · cited by 10,911
Cited by66
Results whose statement or proof uses this declaration.
- Module.IsReflexive.of_isPerfPairstatement · cited by 29
- Module.evalEquivstatement and proof · cited by 14
- LinearEquiv.flipstatement and proof · cited by 10
- RootPairing.root_sub_root_mem_of_pairingIn_posproof · cited by 7
- RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRedproof · cited by 6
- RootPairing.PolarizationEquivproof · cited by 6
- RootPairing.disjoint_rootSpan_ker_rootFormproof · cited by 5
- RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependentproof · cited by 5
- RootPairing.isCompl_rootSpan_ker_rootFormproof · cited by 4
- Module.apply_evalEquiv_symm_applystatement and proof · cited by 4
- Module.bijective_dual_evalstatement and proof · cited by 4
- LinearEquiv.isReflexive_of_equiv_dual_of_isReflexivestatement and proof · cited by 4