Theorems · Definition · linear algebra

Module.evalEquiv

(R : Type u_3) →
  (M : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [Module.IsReflexive R M] → M ≃ₗ[R] Module.Dual R (Module.Dual R M)

The bijection between a reflexive module and its double dual, bundled as a LinearEquiv.

Defined in: Mathlib.LinearAlgebra.Dual.Defs
Cited by: 14 results in Mathlib
Foundations: Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring AddCommMonoid Module Module.IsReflexive

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearEquivstatement · cited by 3,317
Module.Dualstatement · cited by 583
LinearEquiv.ofBijectiveproof · cited by 60
Module.IsReflexivestatement and proof · cited by 58
Module.Dual.evalproof · cited by 52
Module.bijective_dual_evalproof · cited by 4

Cited by16

Results whose statement or proof uses this declaration.

LinearEquiv.flipproof · cited by 10
Module.apply_evalEquiv_symm_applystatement and proof · cited by 4
Module.mapEvalEquivproof · cited by 3
Module.evalEquiv_toLinearMapstatement · cited by 2
LinearMap.flip_injective_iff₁proof · cited by 2
LinearMap.flip_injective_iff₂proof · cited by 2
Subspace.finrank_dualCoannihilator_eqproof · cited by 1
FiniteDimensional.mem_span_of_iInf_ker_le_kerproof · cited by 1
Module.evalEquiv_applystatement · cited by 1
Module.dualMap_dualMap_eq_iff_of_injectiveproof · cited by 1
LinearMap.dualAnnihilator_ker_eq_range_flipproof · cited by 1
Module.Dual.eval_comp_comp_evalEquiv_eqstatement and proof · cited by 0