Commits leanprover-community/mathlib

feat(analysis/ODE): prove Picard-Lindelöf/Cauchy-Lipschitz Theorem (#9791)

urkud committed 4 years ago

773a7a42

feat(topology/sheaves): Pullback of presheaf (#9961)

erdOne committed 4 years ago

74c27b25

chore(data/mv_polynomial/basic): add `map_alg_hom_coe_ring_hom` (#10158)

eric-wieser committed 4 years ago

79eb9344

chore(algebra/direct_sum/internal): add missing simp lemmas (#10154)

eric-wieser committed 4 years ago

11439d8c

feat(data/finset/interval): `finset α` is a locally finite order (#9963)

YaelDillies committed 4 years ago

828e1004

feat(group_theory/sylow): Sylow subgroups are nontrivial! (#10144)

tb65536 committed 4 years ago

cf2ff033

refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` (#9898)

YaelDillies committed 4 years ago

52cd4453

feat(linear_algebra/affine_space/affine_map): decomposition of an affine map between modules as an equiv (#10162)

ocfnash committed 4 years ago

5187a427

chore(data/set): lemmas about `disjoint` (#10148)

urkud committed 4 years ago

22ec295c

split(data/finset/prod): split off `data.finset.basic` (#10142)

YaelDillies committed 4 years ago

69189d44

feat(ring_theory/polynomial/basic): `polynomial.ker_map_ring_hom` and `mv_polynomial.ker_map` (#10160)

eric-wieser committed 4 years ago

de79226c

chore(measure_theory/function/special_functions): import inner_product_space.basic instead of inner_product_space.calculus (#10159)

RemyDegenne committed 4 years ago

2129d053

chore(analysis/calculus/times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155)

ocfnash committed 4 years ago

b8908367

feat(linear_algebra/matrix/nonsingular_inverse): determinant of inverse is inverse of determinant (#10038)

eric-wieser committed 4 years ago

3cbe0feb

feat(topology/algebra/group_with_zero): continuity lemma for division (#9959)

fpvandoorn committed 4 years ago

17afc5c0

feat(data/nat/choose/basic): add some inequalities showing that choose is monotonic in the first argument (#10102)

alexjbest committed 4 years ago

211bdff0

feat(data/list): standardize list prefixes and suffixes (#10052)

EPronovost committed 4 years ago

1f0d878c

feat(topology/homotopy/basic): add `homotopic` for `continuous_map`s. (#9865)

shingtaklam1324 committed 4 years ago

4c0b6ada

chore(data/equiv/mul_add): DRY (#10150)

urkud committed 4 years ago

d219e6bb

chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)

eric-wieser committed 4 years ago

76ba1b64

feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122)

YaelDillies committed 4 years ago

8658f40c

chore(scripts): update nolints.txt (#10146)

leanprover-community-bot committed 4 years ago

4770a6a7

refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129)

YaelDillies committed 4 years ago

0fac0807

refactor(algebra/direct_sum): rework internally-graded objects (#10127)

eric-wieser committed 4 years ago

fed57b54

feat(group_theory/sylow): Sylow subgroups are isomorphic (#10059)

tb65536 committed 4 years ago

6433c1c6

refactor(group_theory/complement): Introduce abbreviation for subgroups (#10009)

tb65536 committed 4 years ago

5541b256

chore(order/lattice): add `exists_lt_of_sup/inf` (#10133)

urkud committed 4 years ago

3a0b0d1d

chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110)

RemyDegenne committed 4 years ago

8f7ffec9

chore(logic/relation): rename to permit dot notation (#10105)

eric-wieser committed 4 years ago

00a1022f

feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096)

sgouezel committed 4 years ago

6993e6f8