Commit 2024-11-18 16:07 72194f73

View on Github →

feat(Algebra): Submodule R A is algebra over Ideal A (#18493) Also upgrade Submodule.mapHom and Ideal.mapHom to RingHoms and show the former is also an AlgHom (Submodule.mapAlgHom).

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.mapHom_id

added theorem Submodule.mul_comm_of_commute

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

added theorem AddSubmonoid.mul_comm_of_commute

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.coe_restrictScalars

modified def Ideal.mapHom

modified theorem Ideal.map_mul

modified theorem Ideal.restrictScalars_mul

Modified Mathlib/RingTheory/Ideal/Operations.lean

added def Submodule.mapAlgEquiv

added def Submodule.mapAlgHom