Commits leanprover-community/mathlib3

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

kim-em committed 3 years ago

cc69e4cc

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

MichaelStollBayreuth committed 3 years ago

389da72f

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

Multramate committed 3 years ago

53541ffc

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

eric-wieser committed 3 years ago

5c430b19

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

mo271 committed 3 years ago

f9a89465

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

8430207e

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

mpenciak committed 3 years ago

a1b06506

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

astrainfinita committed 3 years ago

3a58269b

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

efa2d4cc

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

mariainesdff committed 3 years ago

992c3e50

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

9ee30502

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

RemyDegenne committed 3 years ago

77f0d8b3

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

Paul-Lez committed 3 years ago

917ab03a

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

urkud committed 3 years ago

c57d3b85

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

astrainfinita committed 3 years ago

0de26dbb

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

jsm28 committed 3 years ago

d45bb4b4

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

astrainfinita committed 3 years ago

5901b51c

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

kim-em committed 3 years ago

30f98343

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

pimotte committed 3 years ago

cc99aec2

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

faenuccio committed 3 years ago

4036f521

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

f53bc2a2

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

mcdoll committed 3 years ago

a9781cc8

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

YaelDillies committed 3 years ago

6ef78e60

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

awainverse committed 3 years ago

f2a46a24

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

urkud committed 3 years ago

be769642

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

mariainesdff committed 3 years ago

81da5260

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

jjaassoonn committed 3 years ago

b25a36f9

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

astrainfinita committed 3 years ago

e215a68f

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

astrainfinita committed 3 years ago

e1cef234

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

AntoineChambert-Loir committed 3 years ago

bbefd6e6