Structures · Algebra
Module.Invertible
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
- Shape
- 2 explicit arguments · adds bijective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Localization
How is a type an instance?
Loading the hierarchy index…
Assumed by53
- Module.Invertible.linearEquiv
- CommRing.Pic.mk_eq_iff
- CommRing.Pic.mk_eq_one_iff
- Module.Invertible.free_iff_linearEquiv
- CommRing.Pic.mk.linearEquiv
- Module.Invertible.bijective_of_surjective
- CommRing.Pic.mk_eq_mk_iff
- CommRing.Pic.mk_tensor
- Module.Invertible.linearEquivOfRightInverse
- CommRing.Pic.mk_eq_one_iff_free
- Module.Invertible.finrank_eq_one
- Module.Invertible.rightInverse_of_leftInverse
- Module.Invertible.linearEquivOfLeftInverse
- Module.Invertible.bijective
- Module.Invertible.congr
- Module.Invertible.algEquivOfRing
- CommRing.Pic.mk_dual
- Module.Invertible.leftInverse_of_rightInverse
- Module.Invertible.tensorProductComm_eq_refl
- Module.Invertible.lTensor_surjective_iff
- Module.Invertible.lTensor_injective_iff
- Module.Invertible.instLocalizationLocalizedModule
- Module.Invertible.linearEquivOfRightInverse_symm_apply
- Module.Invertible.instTensorProduct_1
- Module.Invertible.lTensor_bijective_iff
- instInvertibleReprₛ
- Module.Invertible.of_isLocalization
- Module.Invertible.exists_finset_free_localization
- Module.Invertible.tmul_comm
- Module.Invertible.instTensorProduct_2
- Module.Invertible.linearEquivOfLeftInverse_apply
- Module.Invertible.instFinite
- CommRing.Pic.mk.congr_simp
- Module.Invertible.rank_eq_one
- Module.Invertible.rTensor_bijective_iff
- Module.Invertible.instProjective
- Module.Invertible.linearEquivOfRightInverse_apply
- Ideal.eq_top_of_mk_tensor_eq_one
- Module.Invertible.instTensorProduct
- CommRing.Pic.mk_eq_one
- Module.Invertible.linearEquiv.congr_simp
- Module.free_of_isStablyFree_of_invertible
- Module.Invertible.rTensor_surjective_iff
- Module.Invertible.linearEquivOfLeftInverse_symm_apply
- Module.Invertible.exists_linearEquiv_ideal
- Module.Invertible.rTensor_injective_iff
- Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra
- CommRing.Pic.instFreeOfSubsingleton
- Module.Invertible.leftInverse_iff_rightInverse
- Module.Invertible.algEquivOfRing_apply
Ancestors0
No ancestors.