leanprover-community/mathlib3

Pull Requests Commits

trying "Try this", and failing

jcommelin committed 5 years ago

d53a6adf

jcommelin committed 5 years ago

c503e338

jcommelin committed 5 years ago

efb5591e

robertylewis committed 5 years ago

8a5459c5

jcommelin committed 5 years ago

9c7ebfdb

jcommelin committed 5 years ago

a940a031

make side conditions implicit

jcommelin committed 5 years ago

ec9bb8ae

jcommelin committed 5 years ago

e86333a7

jcommelin committed 5 years ago

9f9a0ab0

jcommelin committed 5 years ago

a86b0e07

jcommelin committed 5 years ago

2024688e

long list of lemmas

jcommelin committed 5 years ago

8f85206f

move lemmas to separate file

jcommelin committed 5 years ago

8813486a

jcommelin committed 5 years ago

9ee2fe2b

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

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

fpvandoorn committed 5 years ago

83edb506

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

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

Older