Theorems · Definition · linear algebra
LinearEquiv.dualMap
{R : Type u_1} →
{M₁ : Type u_2} →
{M₂ : Type u_3} →
[inst : CommSemiring R] →
[inst_1 : AddCommMonoid M₁] →
[inst_2 : Module R M₁] →
[inst_3 : AddCommMonoid M₂] →
[inst_4 : Module R M₂] → (M₁ ≃ₗ[R] M₂) → Module.Dual R M₂ ≃ₗ[R] Module.Dual R M₁The LinearEquiv version of LinearMap.dualMap.
- Defined in
- Mathlib.LinearAlgebra.Dual.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- LinearMapproof · cited by 10,215
- LinearEquivstatement and proof · cited by 3,317
- LinearEquiv.symmproof · cited by 1,461
- LinearEquiv.toLinearMapproof · cited by 1,171
- Module.Dualstatement and proof · cited by 583
- LinearMap.dualMapproof · cited by 52
Cited by26
Results whose statement or proof uses this declaration.
- Module.IsReflexive.of_isPerfPairproof · cited by 29
- LinearEquiv.flipproof · cited by 10
- LinearEquiv.isReflexive_of_equiv_dual_of_isReflexiveproof · cited by 4
- Module.Invertible.free_iff_linearEquivproof · cited by 3
- LinearMap.BilinForm.tensorDistribEquivproof · cited by 3
- Module.finite_dual_iffproof · cited by 2
- QuadraticForm.dualProdIsometryproof · cited by 2
- LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjectiveproof · cited by 1
- LinearEquiv.trans_dualMap_symm_flipstatement and proof · cited by 1
- CommRing.Pic.mk_dualproof · cited by 1
- LinearEquiv.dualMap_applystatement · cited by 1
- LinearEquiv.image_closure_of_convexstatement and proof · cited by 1