leanprover-community/mathlib3

Pull Requests Commits

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

feat(data/pnat/basic): Add strong induction on pnat (#4736)

riccardobrasca committed 5 years ago

8255507e

feat(data/list/basic): Add prod_reverse_noncomm (#4757)

eric-wieser committed 5 years ago

c141eed8

feat(algebra/direct_sum): Bundle the homomorphisms (#4754)

eric-wieser committed 5 years ago

4ec88dbe

feat(category_theory): presheaf is colimit of representables (#4401)

b-mehta committed 5 years ago

aa590397

chore(*): a few more type-specific ext lemmas (#4741)

urkud committed 5 years ago

5afeb9b9

fix(deprecated/group): Correct the name of `is_add_group_hom has_neg.neg` (#4755)

eric-wieser committed 5 years ago

0bbf3e29

feat(data/{nat,list}/basic): Add some trivial lemmas (#4738)

eric-wieser committed 5 years ago

58869614

feat(tactic/core): add `run_parser` user command (#4745)

digama0 committed 5 years ago

b651c6f6

fix(deprecated/*): remove instances (#4735)

jcommelin committed 5 years ago

fb4aee0d

Newer Older