Theorem Module.Invertible.tmul_comm

Modification history

2025-11-16 19:18
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): `Module.Invertible.tmul_comm` (#31308)
Added Module.Invertible.tmul_commView on Github →