Theorem CommRing.Pic.mk_dual

Modification history

2025-08-16 08:07

Mathlib/RingTheory/PicardGroup.lean

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

Added CommRing.Pic.mk_dual View on Github →