Theorem CommRing.Pic.mk_self

Modification history

2025-08-16 08:07

Mathlib/RingTheory/PicardGroup.lean

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

Added CommRing.Pic.mk_self View on Github →