Commits leanprover-community/mathlib

feat(number_theory): Dedekind-Kummer theorem (#15000)

Vierkantor committed 3 years ago

1e225257

chore(algebra/order/monoid_lemmas_zero_lt): remove redundant assumptions (#16524)

astrainfinita committed 3 years ago

e763499b

doc(category/abelian/ext): update module doc (#16512)

kim-em committed 3 years ago

7a9e6ca4

feat(number_theory/legendre_symbol/norm_num): add file with `norm_num` extension for the Jacobi symbol (#16519)

MichaelStollBayreuth committed 3 years ago

8922aaa5

refactor(number_theory/padics/padic_val): make prime implicit (#15221)

Multramate committed 3 years ago

894c8c22

feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors (#16153)

eric-wieser committed 3 years ago

d46774d4

feat(archive/100-theorems-list): Stirling, part 2 (#14875)

mo271 committed 3 years ago

fc35e1e9

feat(combinatorics/simple_graph/prod): add `locally_finite` instance for the box product of `locally_finite` graphs, plus two related lemmas (#16431)

bottine committed 3 years ago

104f141e

feat(linear_algebra/symplectic_group): add definition of symplectic group (#15513)

mpenciak committed 3 years ago

a5b382d8

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