Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-21 01:55 0322d892

View on Github →

refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)

Estimated changes

Modified src/analysis/calculus/tangent_cone.lean

Modified src/analysis/normed_space/basic.lean

Modified src/measure_theory/ae_eq_fun.lean

Modified src/measure_theory/borel_space.lean

modified theorem finset.measurable_prod

modified theorem measurable.mul

modified theorem measurable_mul

Modified src/topology/algebra/continuous_functions.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/module.lean

modified theorem continuous_linear_map.add_comp

modified theorem continuous_linear_map.coe_coprod

modified theorem continuous_linear_map.comp_add

modified def continuous_linear_map.coprod

modified theorem continuous_linear_map.coprod_apply

added theorem submodule.eq_top_of_nonempty_interior'

deleted theorem submodule.eq_top_of_nonempty_interior

Modified src/topology/algebra/monoid.lean

Modified src/topology/algebra/multilinear.lean

Modified src/topology/algebra/open_subgroup.lean

modified theorem open_subgroup.is_closed

Modified src/topology/algebra/ring.lean

Modified src/topology/instances/ennreal.lean

Modified test/apply.lean