leanprover-community/mathlib

Pull Requests Commits

Merge branch 'AD_uniform_convergence3' into AD_uniform_convergence_comp

ADedecker committed 3 years ago

0c669207

ADedecker committed 3 years ago

1a6a0af5

Enhance using directedness

ADedecker committed 3 years ago

c6ccec08

ADedecker committed 3 years ago

e1aabac3

chore(data/rat/basic): tidy some proofs (#13603)

Ruben-VandeVelde committed 3 years ago

631890bf

feat(logic/basic): add `auto_param.out` and `opt_param.out` (#13599)

urkud committed 3 years ago

f7dac5ea

feat(set_theory/game/pgame): simp + private (#13596)

vihdzp committed 3 years ago

6729cca2

refactor(data/nat/factorization): Infer arguments (#13595)

vihdzp committed 3 years ago

62205c27

chore(analysis/inner_product_space/lax_milgram): tidy some proofs (#13604)

Ruben-VandeVelde committed 3 years ago

9abfff39

feat(algebra/ring/basic): define non-unital ring homs (#13430)

j-loreaux committed 3 years ago

3d24b093

feat(order/filter/small_sets): define the filter of small sets (#13467)

fpvandoorn committed 3 years ago

394dec32

fix(data/fintype/basic): fix `fintype_of_option_equiv` (#13466)

stuart-presnell committed 3 years ago

9db59165

feat(analysis/calculus/specific_functions): define normed bump functions (#13463)

fpvandoorn committed 3 years ago

0d77f29f

feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444)

eric-wieser committed 3 years ago

06a6044f

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

leanprover-community-bot committed 3 years ago

2b902eb3

feat(data/mv_polynomial/equiv): API for `mv_polynomial.fin_succ_equiv` (#10812)

isadofschi committed 3 years ago

79bc6ad4

feat(polynomial/cyclotomic): `eval_apply` (#13586)

ericrbg committed 3 years ago

17d24243

feat(data/quot): `quotient.out` is injective (#13584)

vihdzp committed 3 years ago

40fc58cb

doc(category_theory/limits/has_limits): fix two docstrings (#13581)

jcommelin committed 3 years ago

821e7c89

chore(set_theory/cardinal/basic): Fix spacing (#13562)

vihdzp committed 3 years ago

7b92db75

fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544)

eric-wieser committed 3 years ago

1da12b57

refactor(category_theory): make has_zero_object a Prop (#13517)

jcommelin committed 3 years ago

77236cd2

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13475)

tb65536 committed 3 years ago

dced1336

chore(*): remove `subst` when not necessary (#13453)

ericrbg committed 3 years ago

bb9d1c50

feat(linear_algebra/prod): two lemmas about prod_map (#13572)

antoinelab01 committed 3 years ago

afb43923

feat(group_theory/transfer): Define the transfer homomorphism (#13446)

tb65536 committed 3 years ago

d444a279

feat(ring_theory/valuation/valuation_subring): The order structure on valuation subrings of a field (#13429)

adamtopaz committed 3 years ago

b1a1ece3

feat(topology/constructions): more convenient lemmas (#13423)

fpvandoorn committed 3 years ago

1e76b9eb

feat(algebra/big_operators): split products and sums over fin (a+b) (#13291)

joelriou committed 3 years ago

63ee5582

feat(group_theory/torsion): torsion-free groups and quotients by torsion subgroups (#13173)

Julian committed 3 years ago

4d7683b2

Older