Theorem Submodule.mul_comm_of_commute

Modification history

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