leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into Mon_in

kim-em committed 5 years ago

807bbd77

feat(algebra/category/Group/*): compare categorical (co)kernels/images with the usual notions (#3443)

kim-em committed 5 years ago

11179d53

feat(logic/basic): mark cast_eq as a `simp` lemma (#3547)

ChrisHughes24 committed 5 years ago

8582b06b

chore(geometry/manifold/real_instance): remove global fact instance (#3549)

sgouezel committed 5 years ago

3484194d

feat(data/num/prime): kernel-friendly decision procedure for prime (#3525)

digama0 committed 5 years ago

e90c7b96

chore(*): minor import cleanup (#3546)

kim-em committed 5 years ago

0379d3ac

feat(topology/*, geometry/*): missing lemmas (#3528)

sgouezel committed 5 years ago

2a456a9c

feat(category_theory/isomorphism): lemmas about cancelling isomorphisms (#3436)

kim-em committed 5 years ago

12a7ce39

feat(data/finsupp): lattice structure on finsupp (#3335)

awainverse committed 5 years ago

2d29f80a

feat(topology/tactic): `continuity` tactic (#2879)

rwbarton committed 5 years ago

8d55eda5

feat(tactic/simps): improvements (#3477)

fpvandoorn committed 5 years ago

6f9da356

chore(ring_theory/prod): move file to algebra/ring/prod (#3540)

ChrisHughes24 committed 5 years ago

4d811493

chore(algebraic_geometry/presheafed_space): use projection rather than fancy coercion (#3507)

kim-em committed 5 years ago

47efcf3c

feat(data/polynomial): irreducible_of_irreducible_mod_prime (#3539)

kim-em committed 5 years ago

229cf6ef

feat(field_theory/fixed): a field is normal over the fixed subfield under a group action (#3520)

kckennylau committed 5 years ago

579b142d

feat(tactic/apply_rules): allow apply_cfg argument (#3538)

kim-em committed 5 years ago

a6ad9043

chore(measure_theory/indicator_function): split into 2 files deps: 3503 (#3509)

urkud committed 5 years ago

2d47d0cb

chore(*): remove `plift` from some lemmas about `infi`/`supr` (#3503)

urkud committed 5 years ago

6fe81bd5

refactor(data/nat/digits): refactor into sections (#3527)

shingtaklam1324 committed 5 years ago

499cb9bb

feat(ring_theory/polynomial/basic): remove unnecessary commutativity assumption (#3535)

jalex-stark committed 5 years ago

5d41ec70

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

leanprover-community-bot committed 5 years ago

c88f8beb

feat(algebra/direct_sum): Add ⨁ notation (#3473)

eric-wieser committed 5 years ago

bad4f978

chore(data/equiv/basic): avoid `λ ⟨a, b⟩` in some defs, add `simp` lemmas (#3530)

urkud committed 5 years ago

289d17cd

refactor(algebra/pi_instance): delete pi_instance file, and move instances to group/ring etc appropriately (#3513)

kim-em committed 5 years ago

2d395a99

chore(measure_theory/l1_space): make `measure` argument of `integrable` optional (#3508)

urkud committed 5 years ago

ed33a99d

chore(order/filter/*): use `[nonempty _]` instead of `(_ : nonempty _)` (#3526)

urkud committed 5 years ago

396a66a0

chore(set_theory/ordinal): split into multiple files (#3517)

sgouezel committed 5 years ago

b9beca0b

refactor(order/filter/at_top): import order.filter.bases (#3523)

urkud committed 5 years ago

79df8cc4

feat(ring_theory/ideal_over): a prime ideal lying over a maximal ideal is maximal (#3488)

Vierkantor committed 5 years ago

d974457e

chore(data/sym2) : simplify proofs (#3522)

jalex-stark committed 5 years ago

7397db78

Older