Commit 2025-11-16 19:18 9f0dc8c6

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

modified theorem IsLocalization.linearMap_compatibleSMul

Modified Mathlib/RingTheory/PicardGroup.lean

added theorem Module.Invertible.tensorProductComm_eq_refl

added theorem Module.Invertible.tmul_comm