Theorem Submodule.mapHom_id

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.mapHom_idView on Github →