Commits leanprover-community/mathlib3

Merge branch 'master' into YK-is-o-pow-exp

urkud committed 3 years ago

532141f5

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

feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete (#16368)

j-loreaux committed 3 years ago

c0ad3bf9

feat(convex/specific_functions): specific case of Jensen's inequality for powers (#16186)

dtumad committed 3 years ago

01a8a9f8

feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum (#15821)

ADedecker committed 3 years ago

3c93c656

feat(data/sym/basic): add `fill` `filter_ne` and `sigma_ext` (#16316)

pimotte committed 3 years ago

a945b376

feat(topology/algebra/order/intermediate_value): intervals are connected (#16473)

jsm28 committed 3 years ago

c64fb26a

feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed (#16303)

j-loreaux committed 3 years ago

4ff10212