leanprover-community/mathlib3

Pull Requests Commits

refactor(data/set/function): Generalize `maps_to`, `inj_on`, `eq_on`, `left_inv_on`, `right_inv_on`, and `inv_on` to anything with has_mem

eric-wieser committed 5 years ago

4ca9b48f

chore(archive/100-theorems-list): 83_friendship_graphs (#5727)

agusakov committed 5 years ago

1509c295

feat(ci): Emit error messages in a way understood by github (#5726)

eric-wieser committed 5 years ago

c8c6d2e7

feat(measure_theory/lebesgue_measure): volume of a box in `ℝⁿ` (#5635)

urkud committed 5 years ago

d11d83ad

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

leanprover-community-bot committed 5 years ago

c050452a

feat(logic/basic): exists_eq simp lemmas without and.comm (#5694)

pechersky committed 5 years ago

71a3261c

feat(data/nat/cast): add nat.bin_cast for faster casting (#5664)

pechersky committed 5 years ago

6397e144

feat(data/set/finite): add lemma with iff statement about when finite sets can be subsets (#5725)

agusakov committed 5 years ago

69e9344c

feat(combinatorics/simple_graph/basic): add definition of common neighbors and lemmas (#5718)

agusakov committed 5 years ago

0b9fbc48

refactor(computability/reduce): define many-one degrees without parameter (#2630)

gebner committed 5 years ago

7ce47174

fix(finsupp/pointwise): Relax the ring requirement to semiring (#5723)

eric-wieser committed 5 years ago

d533fbb5

chore(scripts): don't assume cwd when running lint-style. (#5721)

Julian committed 5 years ago

340ddf83

feat(data/finset): sup_eq_bind (#5717)

kmill committed 5 years ago

d351cfe0

feat(combinatorics/simple_graph/basic): add definition of complement of simple graph (#5697)

agusakov committed 5 years ago

3ac4bb24

feat(analysis/special_functions/pow): add various lemmas about ennreal.rpow (#5701)

RemyDegenne committed 5 years ago

c8574c89

feat(linear_algebra/{exterior,tensor}_algebra): Prove that `ι` is injective (#5712)

eric-wieser committed 5 years ago

b6cca97e

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

leanprover-community-bot committed 5 years ago

b9b6b16c

fix(tactic/ring): fix loop in ring (#5711)

digama0 committed 5 years ago

5a532cab

doc(tactic/generalize_proofs): docs and test for generalize_proofs (#5715)

digama0 committed 5 years ago

fe5ec00e

doc(overview): small reorganization of algebra/number theory (#5707)

jcommelin committed 5 years ago

a7b800ec

chore(analysis|measure_theory|topology): give tsum notation precedence 67 (#5709)

jcommelin committed 5 years ago

c1894c88

feat(data/buffer/parser/basic): lemmas describing parsers (#5460)

pechersky committed 5 years ago

0e7a9214

chore(topology/algebra/infinite_sum): speedup has_sum_sum (#5710)

jcommelin committed 5 years ago

10259082

feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)

eric-wieser committed 5 years ago

73ba4602

docs(undergrad.yaml): analysis updates (#5675)

hrmacbeth committed 5 years ago

e76fdb9e

feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)

eric-wieser committed 5 years ago

ce6a7eba

feat(measure_theory): each set has a measurable superset of the same measure (#5688)

urkud committed 5 years ago

3a3ec6c3

feat(data/set/intervals): add 2 Icc ssubset lemmas (#5617)

Mohamed Al-Fahim committed 5 years ago

26710686

chore(category_theory/limits): move constructions folder (#5681)

b-mehta committed 5 years ago

cd7a8a18

fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)

eric-wieser committed 5 years ago

be75005c

Older