leanprover-community/mathlib

Pull Requests Commits

refactor(linear_algebra/affine_space): allow empty affine subspaces (#3219)

jsm28 committed 5 years ago

a143c386

feat(category/schur): a small corollary of the baby schur's lemma (#3239)

kim-em committed 5 years ago

e250eb41

chore(data/set/intervals): split `I??_union_I??_eq_I??` (#3237)

urkud committed 5 years ago

d788d4b5

chore(algebra/ring): move some classes to `group_with_zero` (#3232)

urkud committed 5 years ago

af53c9d7

chore(data/polynomial): partial move from is_ring_hom to ring_hom (#3213)

kim-em committed 5 years ago

da481e77

feat(data/fintype/basic): card_eq_zero_equiv_equiv_pempty (#3238)

kim-em committed 5 years ago

38904ac8

feat(category_theory): remove nearly all universe annotations (#3221)

kim-em committed 5 years ago

1588d81e

perf(linarith): don't repeat nonneg proofs for nat-to-int casts (#3226)

robertylewis committed 5 years ago

056a72aa

feat(analysis/normed_space/real_inner_product,geometry/euclidean): inner products of weighted subtractions (#3203)

jsm28 committed 5 years ago

791744b0

chore(*): import expression widgets from core (#3181)

gebner committed 5 years ago

4fcd6fd4

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

leanprover-community-bot committed 5 years ago

e8fd085f

chore(*): change notation for `set.compl` (#3212)

urkud committed 5 years ago

45904fba

chore(init_/): remove this directory (#3227)

urkud committed 5 years ago

d3006bad

feat(order/filter/germ): define `filter.germ` (#3172)

urkud committed 5 years ago

eb05a940

feat(algebra/ring): ite_mul_one and ite_mul_zero_... (#3217)

kim-em committed 5 years ago

4907d5d6

feat(data/polynomial): work over noncommutative rings where possible (#3193)

kim-em committed 5 years ago

964f0e53

feat(category/limits/shapes): fix biproducts (#3175)

kim-em committed 5 years ago

a708f854

feat(linear_algebra/affine_space): affine independence (#3140)

jsm28 committed 5 years ago

78beab4f

chore(finset/nat/antidiagonal): simplify some proofs (#3225)

kim-em committed 5 years ago

36ce13fe

feat(linear_algebra/tensor_product): ite_tmul (#3216)

kim-em committed 5 years ago

c4f91767

chore(ring_theory/tensor_product): missing simp lemmas (#3215)

kim-em committed 5 years ago

ca44926c

feat(simp_nf): instructions for linter timeout (#3205)

fpvandoorn committed 5 years ago

a443d8ba

feat(data/padics/padic_norm) Fix namespacing of padic_val_nat (#3207)

Smaug123 committed 5 years ago

9a1c0a6e

feat(data/matrix/notation): smul matrix lemmas (#3208)

pechersky committed 5 years ago

9acf5903

chore(category_theory/punit): use discrete punit instead of punit (#3201)

b-mehta committed 5 years ago

d2b46abb

chore(docs/tutorial): change category declarations (#3220)

agusakov committed 5 years ago

b503fb45

chore(group_theory/submonoid): split into 3 files (#3058)

urkud committed 5 years ago

2ec83dc5

feat(uniform_space): compact uniform spaces, Heine-Cantor (#3180)

PatrickMassot committed 5 years ago

4ad82e5d

chore(measure_theory/outer_measure,measure_space): use `complete_lattice_of_Inf/Sup` (#3185)

urkud committed 5 years ago

3d72c970

fix(tactic/linarith): use refine instead of apply to avoid apply bug (#3199)

robertylewis committed 5 years ago

35fbfe0a

Newer Older