leanprover-community/mathlib3

Pull Requests Commits

Update bernstein.lean

astrainfinita committed 3 years ago

435f2bbe

remove useless lemmas

astrainfinita committed 3 years ago

b6f6a5d2

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

4c2a0bd0

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

578e38b3

Update monoid_lemmas_zero_lt.lean

astrainfinita committed 3 years ago

2fb682fe

Merge branch 'master' into FR_zero_lt_changes

astrainfinita committed 3 years ago

1d73c31a

feat(field_theory/splitting_field): generalize `splits` for `comm_ring K` (#16405)

astrainfinita committed 3 years ago

a0ae2165

chore(category/limits/opposites): instances (#16511)

kim-em committed 3 years ago

53e5dd30

feat(data/sym/basic): add `fill_mem`, `append_mem` and supporting lemmas (#16486)

pimotte committed 3 years ago

a4895002

feat(topology/unit_interval): add lemma add_pos (#16507)

faenuccio committed 3 years ago

fd2fb7b3

feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an `alg_hom` (#16451)

j-loreaux committed 3 years ago

e702f021

docs(analysis/calculus/taylor): Latex fixes (#16508)

mcdoll committed 3 years ago

1afd6c75

refactor(algebra/order/monoid_lemma_zero_lt): Use `{x : α // 0 ≤ α}` (#16447)

YaelDillies committed 3 years ago

660bde43

refactor(model_theory/*): Use `countable` in model theory (#16496)

awainverse committed 3 years ago

0602c598

chore(order/filter/basic): golf (#16472)

urkud committed 3 years ago

d8bc1823

chore(data/finset/powerset): generalize powerset_len_nonempty (#16429)

mariainesdff committed 3 years ago

5cbe3c4f

chore(category_theory/sites/limits): generalise universe level (#16408)

jjaassoonn committed 3 years ago

94b2c2cb

chore(data/mv_polynomial/{basic, monad}): move lemmas `aeval_X_left` and `aeval_X_left_apply` (#16391)

astrainfinita committed 3 years ago

9532aeba

feat(ring_theory/multiplicity): generalize `multiplicity` (#16330)

astrainfinita committed 3 years ago

71b8c46a

refactor (equiv.perm.basic): base of_subtype on extend_domain (#16484)

AntoineChambert-Loir committed 3 years ago

db0c0a79

feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence (#14693)

ADedecker committed 3 years ago

11878a45

chore(number_theory/legendre_symbol/*): move zmod.{legendre|jacobi}_sym* to other namespaces (#16461)

MichaelStollBayreuth committed 3 years ago

e1452ef2

feat(ring_theory/roots_of_unity): add roots_of_unity.norm_one (#16426)

xroblot committed 3 years ago

b118db5c

feat(topology/separation): generalize&rename a lemma (#16503)

urkud committed 3 years ago

a3bb2050

feat(algebra/order/group): some more lemmas about `min`, `max`, and `abs` (#16485)

eric-wieser committed 3 years ago

f9f5d51e

feat(analysis/calculus): Taylor's theorem (#15087)

mcdoll committed 3 years ago

8b8cd99c

feat(analysis/inner_product_space/projection): remove useless `complete_space E` assumption (#15682)

ADedecker committed 3 years ago

2ff92045

fix(order/bounded_order): remove classical axiom from Prop.distrib_lattice (#16497)

alreadydone committed 3 years ago

3d369087

docs(category_theory): mention notation for identity homs (#16410)

jcommelin committed 3 years ago

ed9be880

feat(data/polynomial/eval): add polynomial.map_bit0/1 (#16481)

alexjbest committed 3 years ago

d268bb7a

Older