leanprover-community/mathlib

Pull Requests Commits

docs(order/complete_lattice): make two docstrings more detailed (#4859)

hrmacbeth committed 5 years ago

6f7c5394

refactor(tactic/norm_num): move norm_num extensions (#4822)

digama0 committed 5 years ago

51cbb836

feat(category_theory/sites): functor inclusion constructions (#4845)

b-mehta committed 5 years ago

be161d11

chore(group_theory/group_action): introduce `smul_comm_class` (#4770)

urkud committed 5 years ago

d91c8785

chore(algebra/ordered_group): use implicit args, add `add_eq_coe` (#4853)

urkud committed 5 years ago

9a03bdf1

refactor(order/filter): move some proofs to `bases` (#3478)

urkud committed 5 years ago

e14c3782

chore(data/finset/basic): a few lemmas about `finset.piecewise` (#4852)

urkud committed 5 years ago

f9c8abe3

chore(linear_algebra/affine_space/ordered): compare endpoints to midpoint (#4851)

urkud committed 5 years ago

7756265e

feat(linear_algebra/affine_space/affine_map): add `affine_map.proj` (#4850)

urkud committed 5 years ago

1f616214

refactor(data/pnat): move data.pnat.prime (#4839)

digama0 committed 5 years ago

6a449305

feat(data/dfinsupp): Port `finsupp.lsum` and lemmas about `lift_add_hom` (#4833)

eric-wieser committed 5 years ago

3b2c97f9

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq (#4810)

eric-wieser committed 5 years ago

17697a60

feat(analysis/normed_space/add_torsor): distance to midpoint (#4849)

urkud committed 5 years ago

67c2b5a0

feat(order/conditionally_complete_lattice): nested intervals lemma (#4848)

urkud committed 5 years ago

1521da68

feat(algebra/module/ordered): add pi instance (#4847)

urkud committed 5 years ago

f5fd2186

feat(category_theory/sites): generate lemmas (#4840)

b-mehta committed 5 years ago

6fc35175

feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)

tb65536 committed 5 years ago

517f0b5c

feat(data/prod): comp_map (#4826)

pechersky committed 5 years ago

0f39d7ad

chore(order/filter/bases): golf a proof (#4834)

urkud committed 5 years ago

2283cf06

feat(analysis/calculus/times_cont_diff): differentiability of field inverse (#4795)

urkud committed 5 years ago

94fa9058

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

leanprover-community-bot committed 5 years ago

d5650a7f

feat(data/polynomial/lifts): polynomials that lift (#4796)

riccardobrasca committed 5 years ago

cc7f06bd

feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)

eric-wieser committed 5 years ago

bfadf057

feat(number_theory/fermat4): The n=4 case of fermat (#4720)

paulvanwamelen committed 5 years ago

58f8817e

feat(ring_theory/witt_vector/is_poly): supporting ghost calculations (#4691)

jcommelin committed 5 years ago

d28e3d10

feat(field_theory/intermediate_field): equalities from inclusions and dimension bounds (#4828)

tb65536 committed 5 years ago

3aac0287

feat(data/polynomial): ext lemmas for homomorphisms from `polynomial R` (#4823)

urkud committed 5 years ago

6ec7aece

feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821)

eric-wieser committed 5 years ago

03a477c4

feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)

eric-wieser committed 5 years ago

5ae192eb

chore(topology/basic): the set of cluster pts of a filter is a closed set (#4815)

urkud committed 5 years ago

d46d0c27

Newer Older