Commits leanprover-community/mathlib

fix(tactic/monotonicity/interactive): fix the order of calling `unify_with_instance` (#16480)

astrainfinita committed 3 years ago

69be6fe3

feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ (#16488)

j-loreaux committed 3 years ago

f1397dc1

feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm (#14115)

mariainesdff committed 3 years ago

97befb83

feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals (#16446)

j-loreaux committed 3 years ago

3077b72c

feat(probabiliy/martingale): centering lemma (#16517)

RemyDegenne committed 3 years ago

54882236

feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 (#16450)

Paul-Lez committed 3 years ago

2178a7f7

chore(topology/separation): move/add `simp` lemmas (#16470)

urkud committed 3 years ago

0f287f82

feat(data/polynomial/eval): add `map_{eq/ne}_zero_iff` (#16440)

astrainfinita committed 3 years ago

400aa375

feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378)

jsm28 committed 3 years ago

7afe23e0

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