Commit 2024-05-19 22:31 df27b2d7

View on Github →

feat: remove useless assumption in continuous_algebraMap (#13015)

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

modified theorem continuousSMul_of_algebraMap

modified theorem continuous_algebraMap

modified theorem continuous_algebraMap_iff_smul