Theorem CommRing.Pic.subsingleton_iff

Modification history

2025-11-20 10:13

Mathlib/RingTheory/PicardGroup.lean

feat(Algebra): generalize Picard group to Semiring (#30657)

Modified CommRing.Pic.subsingleton_iff View on Github →

2025-08-16 08:07

Mathlib/RingTheory/PicardGroup.lean

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

Added CommRing.Pic.subsingleton_iff View on Github →