Commit 2022-02-18 04:52 17b3357b

View on Github →

feat(topology/algebra): generalize has_continuous_smul arguments to has_continuous_const_smul (#11999) This changes the majority of the downstream call-sites of the const_smul lemmas to only need the weaker typeclass.

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/complex/cauchy_integral.lean

Modified src/analysis/convex/strict.lean

modified theorem strict_convex.affinity

modified theorem strict_convex.smul

Modified src/analysis/convex/topology.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/operator_norm.lean

modified def continuous_linear_map.prodₗᵢ

Modified src/dynamics/minimal.lean

modified theorem is_compact.exists_finite_cover_smul

modified theorem is_minimal_iff_closed_smul_invariant

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/function/ae_eq_fun.lean

Modified src/measure_theory/group/action.lean

Modified src/measure_theory/measure/complex.lean

Modified src/measure_theory/measure/vector_measure.lean

modified theorem measure_theory.vector_measure.absolutely_continuous.smul

modified theorem measure_theory.vector_measure.mutually_singular.smul_left

modified theorem measure_theory.vector_measure.mutually_singular.smul_right

Modified src/topology/algebra/affine.lean

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/module/basic.lean

Modified src/topology/algebra/module/multilinear.lean

Modified src/topology/algebra/module/weak_dual.lean

Modified src/topology/continuous_function/locally_constant.lean

modified def locally_constant.to_continuous_map_alg_hom

modified def locally_constant.to_continuous_map_linear_map