Commit 2025-11-20 10:13 49aa5eed

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Skeleton.lean

added def CategoryTheory.Skeletal.monoidHom

added def CategoryTheory.Skeletal.mulEquiv

deleted def CategoryTheory.commMonoidOfSkeletalBraided

Modified Mathlib/RingTheory/PicardGroup.lean

modified theorem CommRing.Pic.subsingleton_iff

added theorem CommRing.Pic.subsingleton_iffₛ

modified def CommRing.Pic