Commit 2023-02-11 10:10 a51b46b4

View on Github →

fix: rename HasContinuousConstSMul to ContinuousConstSMul (#2185)

Estimated changes

Modified Mathlib/Dynamics/Minimal.lean

modified theorem IsCompact.exists_finite_cover_smul

modified theorem isMinimal_iff_closed_smul_invariant

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem ContinuousConstSMul.secondCountableTopology

deleted theorem HasContinuousConstSMul.secondCountableTopology

modified theorem IsCompact.smul

modified theorem isOpenMap_quotient_mk'_mul