Commit 2025-08-16 08:07 c776b599

View on Github →

feat(RingTheory): invertible modules and Picard group (#25337)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

Created Mathlib/RingTheory/PicardGroup.lean

added theorem CommRing.Pic.ext_iff

added theorem CommRing.Pic.inv_eq_dual

added theorem CommRing.Pic.mk_dual

added theorem CommRing.Pic.mk_eq_iff

added theorem CommRing.Pic.mk_eq_mk_iff

added theorem CommRing.Pic.mk_eq_one

added theorem CommRing.Pic.mk_eq_one_iff

added theorem CommRing.Pic.mk_eq_self

added theorem CommRing.Pic.mk_self

added theorem CommRing.Pic.mk_tensor

added theorem CommRing.Pic.mul_eq_tensor

added theorem CommRing.Pic.subsingleton_iff

added def CommRing.Pic

added theorem Module.Invertible.bijective_curry

added theorem Module.Invertible.bijective_of_surjective

added theorem Module.Invertible.embAlgebra_injective

added theorem Module.Invertible.finrank_eq_one

added theorem Module.Invertible.free_iff_linearEquiv

added theorem Module.Invertible.lTensor_bijective_iff

added theorem Module.Invertible.lTensor_injective_iff

added theorem Module.Invertible.lTensor_surjective_iff

added theorem Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm

added theorem Module.Invertible.rTensorInv_injective

added theorem Module.Invertible.rTensorInv_leftInverse

added theorem Module.Invertible.rTensor_bijective_iff

added theorem Module.Invertible.rTensor_injective_iff

added theorem Module.Invertible.rTensor_surjective_iff

added theorem Module.Invertible.rank_eq_one

added theorem Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm

added theorem Module.Invertible.toModuleEnd_bijective

added theorem Submodule.projective_of_isUnit

added theorem Units.submodule_invertible

Modified docs/references.bib