Commit 2025-11-24 11:02 d6715ef8

View on Github →

feat(Topology): generalize IsModuleTopology lemmas to semilinear maps (#31429)

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem continuousSMul_inducedₛₗ

Modified Mathlib/Topology/Algebra/Module/ModuleTopology.lean

modified theorem IsModuleTopology.continuous_of_distribMulActionHom

added theorem IsModuleTopology.continuous_of_distribMulActionHomₑ

added theorem IsModuleTopology.continuous_of_linearMapₛₗ

added theorem IsModuleTopology.isOpenMap_of_surjectiveₛₗ

added theorem IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗ

added theorem IsModuleTopology.isQuotientMap_of_surjectiveₛₗ

deleted theorem IsModuleTopology.iso

added theorem ModuleTopology.eq_coinduced_of_surjectiveₛₗ