Theorems · Inductive type · commutative algebra
Module.Invertible
(R : Type u) → (M : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
An R-module M is invertible if the canonical map Mᵛ ⊗[R] M → R is an isomorphism,
where Mᵛ is the R-dual of M.
- Defined in
- Mathlib.RingTheory.PicardGroup
- Cited by
- 41 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 by49
Results whose statement or proof uses this declaration.
- CommRing.Pic.mkstatement and proof · cited by 17
- Module.Invertible.linearEquivstatement and proof · cited by 8
- CommRing.Pic.mk_eq_iffstatement and proof · cited by 5
- CommRing.Pic.mk_eq_one_iffstatement and proof · cited by 4
- CommRing.Pic.mk.linearEquivstatement and proof · cited by 3
- Module.Invertible.bijective_of_surjectivestatement and proof · cited by 3
- Module.Invertible.free_iff_linearEquivstatement and proof · cited by 3
- CommRing.Pic.mk_eq_mk_iffstatement and proof · cited by 3
- Module.Invertible.finrank_eq_onestatement and proof · cited by 2
- CommRing.Pic.mk_eq_one_iff_freestatement and proof · cited by 2
- CommRing.Pic.mk_tensorstatement and proof · cited by 2
- Module.Invertible.linearEquivOfLeftInversestatement and proof · cited by 2