Theorem CommRing.Pic.Submodule.mulExact_unitsMap_spanSingleton_unitsToPic

Modification history

2026-01-11 09:23
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup (#30736)
Added CommRing.Pic.Submodule.mulExact_unitsMap_spanSingleton_unitsToPicView on Github →