leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/affine_space/combination): `sdiff`, `subtype`, `filter` lemmas (#16644)

jsm28 committed 4 years ago

b8e7a8d9

feat(tactic/positivity): Handle `a ≠ 0` assumptions (#16529)

YaelDillies committed 4 years ago

caf8c55f

feat(ring_theory/mv_polynomial/tower): add analogs of existing lemmas for `mv_polynomial` (#16412)

astrainfinita committed 4 years ago

609b9346

feat(linear_algebra/affine_space/finite_dimensional): `collinear` lemmas, implicit arguments (#16332)

jsm28 committed 4 years ago

2eac7392

feat(logic/equiv/fin): `succ_above` as an equivalence (#16278)

jsm28 committed 4 years ago

5abbfc93

feat(geometry/euclidean/basic): bundled spheres (#16184)

jsm28 committed 4 years ago

a4d24238

feat(ring_theory/filtration): Artin-Rees lemma and Krull's intersection theorems (#16000)

erdOne committed 4 years ago

e24808b3

feat(algebra/char_p/mixed_char_zero): define mixed/equal characteristic zero (#14672)

Jon Eugster committed 4 years ago

96782a2d

feat(data/finset/prod): `finset.diag` and `finset.off_diag` lemmas (#16808)

YaelDillies committed 4 years ago

8a8470cc

feat(category_theory/limits): bicartesian squares (#14375)

kim-em committed 4 years ago

52a270e2

chore(algebra/hom/non_unital_alg): add missing `non_unital_ring_hom_class` instance (#16783)

j-loreaux committed 4 years ago

ae17d05f

feat(ring_theory/ideal/minimal_prime): Minimal prime ideals over an ideal (#16136)

erdOne committed 4 years ago

8f83c26d

feat(data/set/prod): `set.off_diag` (#16803)

YaelDillies committed 4 years ago

e36ae183

fix(docs/references.bib): fix Fröhlich's name in the references (#16802)

faenuccio committed 4 years ago

3946a602

chore(topology/algebra/polynomial): golf `polynomial.coeff_le_of_roots_le` (#16789)

alreadydone committed 4 years ago

8f40883e

feat(data/{finsupp,pi}/lex): generalize from linear_order to partial_order (#16740)

alreadydone committed 4 years ago

5c88020d

feat(number_theory/padic_numbers): bundle padic_norm_e (#16650)

ericrbg committed 4 years ago

6858e178

chore(data/complex/basic): golf 2 proofs (#16788)

urkud committed 4 years ago

b2e818bb

feat(tactic/qify) : `qify` tactic (#16313)

Biiiilly committed 4 years ago

9fe85cd0

feat(tactic/positivity): Extension for `int.nat_abs` (#16787)

YaelDillies committed 4 years ago

91df768e

feat(algebra/monoid_algebra/support): lemmas about support and multiplying with single (#16326)

adomani committed 4 years ago

16749fc4

refactor(algebra/symmetrized): Bundle `sym` and `unsym` as equivalences (#14334)

YaelDillies committed 4 years ago

93354783

refactor(order/succ_pred/limit): redefine successor/predecessor limits (#15655)

vihdzp committed 4 years ago

7aaa53f7

chore(scripts): update nolints.txt (#16793)

leanprover-community-bot committed 4 years ago

efb178db

feat(overview.yaml): add divergence theorem (#16781)

fpvandoorn committed 4 years ago

3f6d1de3

feat(ring_theory/roots_of_unity): add geom_sum_eq_zero (#16755)

riccardobrasca committed 4 years ago

8230606c

feat(order/antisymmetrization): (<) is well-founded for a preorder iff well-founded on its antisymmetrization (#16741)

alreadydone committed 4 years ago

522ace49

refactor(data/list/count): review API, add lemmas (#16736)

urkud committed 4 years ago

561202d0

feat(analysis/inner_product_space/pi_L2): extend an indexed orthonormal set to an orthonormal basis (#16478)

hrmacbeth committed 4 years ago

b5ce4aa2

feat(algebra/free_monoid): action of the `free_monoid` (#16746)

urkud committed 4 years ago

41a72546

Newer Older