Theorems · Theorem · linear algebra

Module.dualMap_dualMap_eq_iff

∀ (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' : Type u_6} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.IsReflexive R M']
  {f g : M →ₗ[R] M'}, f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

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

Mathlib docs Source Loogle LeanSearch

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.

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
LinearMapstatement and proof · cited by 10,215
Module.Dualstatement · cited by 583
Function.Bijective.injectiveproof · cited by 115
Module.IsReflexivestatement and proof · cited by 58
LinearMap.dualMapstatement · cited by 52
Module.bijective_dual_evalproof · cited by 4
Module.dualMap_dualMap_eq_iff_of_injectiveproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

RootPairing.Hom.coweightHom_injectiveproof · cited by 1