leanprover-community/mathlib

Pull Requests Commits

feat(data/equiv/basic): subsingleton equiv and perm (#5736)

pechersky committed 5 years ago

64a1b197

feat(order): closure operators (#5524)

b-mehta committed 5 years ago

975f41a4

feat(measure_theory): absolute continuity of the integral (#5743)

urkud committed 5 years ago

0817e7fe

feat(linear_algebra/{exterior,tensor,free}_algebra): provide left-inverses for `algebra_map` and `ι` (#5722)

eric-wieser committed 5 years ago

3b8cfdc9

chore(data/equiv/fin): simp definitional lemmas (#5740)

pechersky committed 5 years ago

91b099eb

feat(control/equiv_functor): simp defn lemmas and injectivity (#5739)

pechersky committed 5 years ago

7e9094b1

chore(data/equiv/basic): swap symm and trans simp lemmas (#5738)

pechersky committed 5 years ago

e3cc92e1

chore(group_theory/perm/sign): trans and symm simp (#5735)

pechersky committed 5 years ago

de8b88f1

chore(data/set/basic): reuse some proofs about `boolean_algebra` (#5728)

urkud committed 5 years ago

82532c19

refactor(measure_theory): review def&API of the `dirac` measure (#5732)

urkud committed 5 years ago

3b3f9a21

feat(algebra/order): ne_iff_lt_iff_le

pechersky committed 5 years ago

8bc26d13

chore(*): split some long lines (#5742)

urkud committed 5 years ago

159542ad

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

Newer Older