Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-05-19 17:40
f2534017
View on Github →
refactor: coherent composition order (
#1055
)
Estimated changes
Modified
src/analysis/asymptotics.lean
Modified
src/analysis/complex/exponential.lean
Modified
src/analysis/normed_space/banach.lean
Modified
src/analysis/normed_space/basic.lean
Modified
src/analysis/normed_space/deriv.lean
Modified
src/analysis/specific_limits.lean
Modified
src/data/padics/hensel.lean
Modified
src/measure_theory/borel_space.lean
Modified
src/measure_theory/decomposition.lean
Modified
src/order/filter/basic.lean
Modified
src/topology/algebra/group.lean
Modified
src/topology/algebra/group_completion.lean
Modified
src/topology/algebra/infinite_sum.lean
Modified
src/topology/algebra/monoid.lean
Modified
src/topology/algebra/ordered.lean
Modified
src/topology/algebra/uniform_group.lean
Modified
src/topology/basic.lean
added
theorem
inter_mem_nhds_within
added
theorem
nhds_within_restrict'
Modified
src/topology/constructions.lean
Modified
src/topology/instances/complex.lean
Modified
src/topology/instances/ennreal.lean
Modified
src/topology/instances/nnreal.lean
Modified
src/topology/instances/real.lean
Modified
src/topology/metric_space/basic.lean
Modified
src/topology/metric_space/completion.lean
Modified
src/topology/metric_space/gromov_hausdorff.lean
Modified
src/topology/metric_space/lipschitz.lean
Modified
src/topology/order.lean
added
theorem
continuous_at.comp
modified
theorem
continuous_on.comp
added
theorem
continuous_within_at.comp
Modified
src/topology/sequences.lean
Modified
src/topology/uniform_space/basic.lean
Modified
src/topology/uniform_space/completion.lean
Modified
src/topology/uniform_space/separation.lean