Commit 2024-01-16 21:01 0bd32e0c

View on Github →

feat: basic theory connecting R[X]-submodules and invariant R-submodules (#9721)

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

added theorem Submodule.toAddSubmonoid_sSup

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

added def Submodule.restrictScalarsLatticeHom

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

added theorem Polynomial.aeval_apply_smul_mem_of_le_comap'

added theorem Polynomial.aeval_apply_smul_mem_of_le_comap

Modified Mathlib/Data/Polynomial/Module.lean

added theorem Module.AEval.C_smul

added def Module.AEval.comapSubmodule

added theorem Module.AEval.comapSubmodule_le_comap

added theorem Module.AEval.comapSubmodule_mapSubmodule

added def Module.AEval.mapSubmodule

added theorem Module.AEval.mapSubmodule_comapSubmodule

added theorem Module.AEval.mem_comapSubmodule

added theorem Module.AEval.mem_mapSubmodule

Modified Mathlib/Order/Hom/CompleteLattice.lean

added def OrderIso.toCompleteLatticeHom