Theorem AddSubmonoid.mul_comm_of_commute

Modification history

2024-11-18 16:07
Mathlib/Algebra/Group/Submonoid/Pointwise.lean
feat(Algebra): `Submodule R A` is algebra over `Ideal A` (#18493) …
Added AddSubmonoid.mul_comm_of_commuteView on Github →