Theorem CommRing.Pic.Module.Flat.toAlgebra_injective

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.Module.Flat.toAlgebra_injective View on Github →