Commit 2026-01-11 09:23 5660741e

View on Github →

feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup (#30736)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/RingTheory/PicardGroup.lean

added theorem CommRing.Pic.Module.Flat.toAlgebra_injective

added theorem CommRing.Pic.Module.Flat.top_mul_submoduleAlgebra

added theorem CommRing.Pic.Module.Invertible.exists_linearEquiv_ideal

added theorem CommRing.Pic.Module.Invertible.tensorProductComm_eq_refl

added theorem CommRing.Pic.Module.Invertible.tmul_comm

added theorem CommRing.Pic.Submodule.ker_unitsToPic

added theorem CommRing.Pic.Submodule.mulExact_unitsMap_spanSingleton_unitsToPic

added theorem CommRing.Pic.Submodule.mulExact_unitsToPic_mapAlgebra

added theorem CommRing.Pic.Submodule.projective_of_isUnit

added theorem CommRing.Pic.Submodule.range_unitsToPic

added theorem CommRing.Pic.mapAlgebra_comp_mapAlgebra

added theorem CommRing.Pic.mapAlgebra_mapAlgebra

added theorem CommRing.Pic.mapAlgebra_self

added theorem CommRing.Pic.mapAlgebra_self_apply

added theorem CommRing.Pic.mapRingHom_algebraMap

added theorem CommRing.Pic.mapRingHom_comp_mapRingHom

added theorem CommRing.Pic.mapRingHom_id

added theorem CommRing.Pic.mapRingHom_id_apply

added theorem CommRing.Pic.mapRingHom_mapRingHom

modified theorem CommRing.Pic.mk_eq_one

added theorem CommRing.Pic.mk_eq_one_iff_free

added theorem CommRing.Pic.relPic_eq_top

deleted theorem Module.Invertible.embAlgebra_injective

deleted theorem Module.Invertible.tensorProductComm_eq_refl

deleted theorem Module.Invertible.tmul_comm

deleted theorem Submodule.projective_of_isUnit

deleted theorem Units.submodule_invertible