Def Submodule.mapAlgEquiv

Modification history

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