Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-05-17 16:13
0b350228
View on Github →
refactor: change variables order in some composition lemmas (
#1035
)
Estimated changes
Modified
src/analysis/complex/exponential.lean
Modified
src/analysis/complex/polynomial.lean
Modified
src/analysis/normed_space/basic.lean
Modified
src/analysis/normed_space/deriv.lean
added
theorem
has_fderiv_at.comp_has_fderiv_within_at
deleted
theorem
has_fderiv_within_at.comp_has_fderiv_at
Modified
src/category_theory/concrete_category.lean
Modified
src/measure_theory/borel_space.lean
Modified
src/measure_theory/giry_monad.lean
Modified
src/measure_theory/integration.lean
Modified
src/measure_theory/measurable_space.lean
Modified
src/measure_theory/measure_space.lean
modified
theorem
measure_theory.measure.map_map
Modified
src/topology/algebra/continuous_functions.lean
Modified
src/topology/algebra/group.lean
Modified
src/topology/algebra/group_completion.lean
Modified
src/topology/algebra/monoid.lean
Modified
src/topology/algebra/ring.lean
Modified
src/topology/algebra/uniform_group.lean
Modified
src/topology/algebra/uniform_ring.lean
Modified
src/topology/basic.lean
modified
theorem
continuous.comp
Modified
src/topology/bounded_continuous_function.lean
Modified
src/topology/compact_open.lean
modified
def
continuous_map.induced
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/maps.lean
modified
theorem
embedding_compose
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/isometry.lean
modified
theorem
isometry.comp
Modified
src/topology/uniform_space/completion.lean
modified
theorem
uniform_space.completion.map_comp