Theorem Module.Invertible.tensorProductComm_eq_refl

Modification history

2026-01-11 09:23

Mathlib/RingTheory/PicardGroup.lean

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

Deleted Module.Invertible.tensorProductComm_eq_refl View on Github →

2025-11-16 19:18

Mathlib/RingTheory/PicardGroup.lean

feat(RingTheory): `Module.Invertible.tmul_comm` (#31308)

Added Module.Invertible.tensorProductComm_eq_refl View on Github →