Theorem AddSubmonoid.mul_comm_of_commute

Modification history

2025-04-09 09:39
Mathlib/Algebra/Group/Submonoid/Pointwise.lean
chore(Algebra/Group/Subgroup/Pointwise): don't import `GroupWithZero` (#23832) …
Modified AddSubmonoid.mul_comm_of_commuteView on Github →
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 →