Theorem Submodule.projective_of_isUnit

Modification history

2026-01-11 09:23
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup (#30736)
Deleted Submodule.projective_of_isUnitView on Github →
2025-08-16 08:07
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): invertible modules and Picard group (#25337)
Added Submodule.projective_of_isUnitView on Github →