Theorem CommRing.Pic.subsingleton_iffₛ

Modification history

2025-11-20 10:13
Mathlib/RingTheory/PicardGroup.lean
feat(Algebra): generalize Picard group to Semiring (#30657)
Added CommRing.Pic.subsingleton_iffₛView on Github →