Mathlib Changelog
v3
Changelog
About
Github
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