leanprover-community/mathlib3

Pull Requests Commits

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

feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (#4751)

urkud committed 5 years ago

a9d3ce8e

fix(tactic/core): fix infinite loop in emit_code_here (#4746)

digama0 committed 5 years ago

e7a4b12c

chore(linear_algebra/tensor_product): missing simp lemmas (#4769)

jcommelin committed 5 years ago

151f0dd2

chore(ring_theory/unique_factorization_domain): fix some lemma names (#4765)

awainverse committed 5 years ago

69f550cb

chore(algebra/group/pi): add `pi.has_div` (#4776)

urkud committed 5 years ago

14cff9ac

chore(analysis/normed_space): add 2 `@[simp]` attrs (#4775)

urkud committed 5 years ago

f056468f

feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764)

eric-wieser committed 5 years ago

cae77dc7

feat(ring_theory/polynomial/content): `gcd_monoid` instance on polynomials over gcd domain (#4760)

awainverse committed 5 years ago

de6a9d41

feat(data/polynomial/ring_division): Two easy lemmas about polynomials (#4742)

riccardobrasca committed 5 years ago

570c293a

feat(linear_algebra/nonsingular_inverse): add stronger form of Cramer's rule (#4737)

Oliver Nash committed 5 years ago

b9a94d69

fix(tactic/core): use eval_pexpr in run_parser_cmd (#4761)

digama0 committed 5 years ago

2987a496

Older