Commits leanprover-community/mathlib

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

chore(ring_theory/local_properties): remove coercions from `ring_hom` to `monoid_hom` (#16453)

eric-wieser committed 3 years ago

5bd4f627

feat(data/complex/module): define `real_part` and `imaginary_part` (#16438)

j-loreaux committed 3 years ago

06ae0493

feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

Paul-Lez committed 3 years ago

36e01301

feat(data/nat/{choose/multinomial,factorial/big_operations}): add multinomial coefficient definition with basic lemma's (#16170)

pimotte committed 3 years ago

a280c1e5

chore(linear_algebra): rename dual_pair (#16482)

PatrickMassot committed 3 years ago

1b3556cc

feat(analysis/inner_product_space/pi_L2): change of basis matrix between orthonormal bases is unitary (#16474)

hrmacbeth committed 3 years ago

f058af30

feat(algebra/algebra/basic): add two simp lemmas (#16096)

Paul-Lez committed 3 years ago

38963b53

chore(data/real/cau_seq_completion): golf using existing lemmas (#16469)

eric-wieser committed 3 years ago

60f72157

feat(data/polynomial/algebra_map): add `aeval_X_left_apply` (#16433)

astrainfinita committed 3 years ago

86be023b

feat(analysis/normed/group/seminorm): Group norms (#16237)

YaelDillies committed 3 years ago

28b23c94

feat(data/real/ennreal): Add `to_real_{min, sup, inf}` (#16233)

linesthatinterlace committed 3 years ago

e1847377

refactor(set_theory/basic): match `x < ℵ₀` lemmas with `x ≤ ℵ₀` lemmas (#15662)

vihdzp committed 3 years ago

1c4e1843

feat(linear_algebra/finsupp): A variant of `finsupp.total` for `fintype`s. (#15462)

erdOne committed 3 years ago

d5ef0684

feat(measure_theory/function/conditional_expectation): conditional expectation with respect to the bot sigma algebra (#16342)

RemyDegenne committed 3 years ago

745e23d5

feat(data/{seq,stream}): cons_injective2 (#15832)

vihdzp committed 3 years ago

3c006126