Theorem Module.Invertible.tensorProductComm_eq_refl

Modification history

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