leanprover-community/mathlib

Pull Requests Commits

Merge branch 'bundeld-eval-PRd' into bundled-eval

urkud committed 5 years ago

0674db29

Merge branch 'bundled-monomial' into bundeld-eval-PRd

urkud committed 5 years ago

c5b1c99e

Merge branch 'linft-nc-smul' into bundeld-eval-PRd

urkud committed 5 years ago

30250a7e

refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762)

urkud committed 5 years ago

e0b153b2

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

leanprover-community-bot committed 5 years ago

69db7a33

chore(*): reflow some long lines (#4794)

urkud committed 5 years ago

6e2980ce

feat(data/equiv/basic): equiv.set.powerset (#4790)

digama0 committed 5 years ago

8746f083

feat(degree/basic.lean): degree_lt_iff_coeff_zero (#4792)

tb65536 committed 5 years ago

c76c3c5c

fix(tactic/derive_fintype): add support for props (#4777)

digama0 committed 5 years ago

95b3add2

feat(tactic/rcases): add `rintro (x y : t)` support (#4722)

digama0 committed 5 years ago

94285983

feat(ring_theory/finiteness): some finiteness notions in commutative algebra (#4634)

jcommelin committed 5 years ago

877a20e3

chore(algebra/module,linear_algebra): split off a `linear_map` file (#4476)

Vierkantor committed 5 years ago

61c095f2

urkud committed 5 years ago

2bf5b298

feat(simps): improve error messages (#4653)

fpvandoorn committed 5 years ago

83edb506

Merge branch 'master' into bundled-monomial

urkud committed 5 years ago

dfa260c3

feat(data/dfinsupp): Add missing to_additive lemmas (#4788)

eric-wieser committed 5 years ago

ba5594a6

feat(ring_theory/witt_vector/basic): verifying the ring axioms (#4694)

jcommelin committed 5 years ago

2e90c600

Merge branch 'master' into bundled-monomial

urkud committed 5 years ago

1231c721

urkud committed 5 years ago

2331d702

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

leanprover-community-bot committed 5 years ago

7be82f94

chore(order/galois_connection): define `with_bot.gi_get_or_else_bot` (#4781)

urkud committed 5 years ago

b2b39edd

chore(algebra/group/hom): use `coe_comp` in `simp` lemmas (#4780)

urkud committed 5 years ago

121c9a49

chore(data/polynomial/{degree/basic, eval}): Some trivial lemmas about polynomials (#4768)

riccardobrasca committed 5 years ago

6e4fe98c

feat(algebra/big_operators/nat_antidiagonal): a few more lemmas (#4783)

urkud committed 5 years ago

40362122

urkud committed 5 years ago

7bf8fd20

urkud committed 5 years ago

e208d9aa

Merge branch 'degree-gi' into bundled-monomial

urkud committed 5 years ago

76c426ce

Merge branch 'polylemmas' into bundled-monomial

urkud committed 5 years ago

70ea8819

urkud committed 5 years ago

5ee13724

Merge branch 'eval-PRd' into bundled-eval

urkud committed 5 years ago

9db082e5

Newer Older