leanprover-community/mathlib

Pull Requests Commits

fix(algebra/pi_instances): improve definitions of `pi.*` (#3116)

urkud committed 5 years ago

f0593365

feat(data/finset,data/fintype,algebra/big_operators): some more lemmas (#3124)

jsm28 committed 5 years ago

54cc126b

feat(analysis/calculus): C^1 implies strictly differentiable (#3119)

hrmacbeth committed 5 years ago

86dcd5cd

feat(linear_algebra/affine_space): affine combinations for finsets (#3122)

jsm28 committed 5 years ago

46a88944

feat(linear_algebra/matrix): trace of an endomorphism independent of basis (#3125)

kckennylau committed 5 years ago

105fa176

chore(data/finmap): nolint (#3131)

bryangingechen committed 5 years ago

068aaafa

refactor(ring_theory/*): make PID class a predicate (#3114)

kbuzzard committed 5 years ago

3f9b52ae

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

leanprover-community-bot committed 5 years ago

6aba9580

chore(data/list/alist): nolint (#3129)

bryangingechen committed 5 years ago

d59adc18

fix(tactic/delta_instance): bug in computing pi arity (#3127)

robertylewis committed 5 years ago

5b5ff790

feat(topology/uniform_space): some basic lemmas (#3123)

PatrickMassot committed 5 years ago

eff9ed3a

feat(tactic/cancel_denoms): try to remove numeral denominators (#3109)

robertylewis committed 5 years ago

7073c8b9

feat(tactic/zify): move nat propositions to int (#3108)

robertylewis committed 5 years ago

b7d056a1

fix(tactic/set): use provided type for new variable (#3126)

robertylewis committed 5 years ago

d097161b

feat(tactic/simps): option `trace.simps.verbose` prints generated lemmas (#3121)

cipher1024 committed 5 years ago

8729fe21

feat(*): random lemmas about sets and filters (#3118)

PatrickMassot committed 5 years ago

e8ff6ff6

fix(tactic/group): bugfix for inverse of 1 (#3117)

alexjbest committed 5 years ago

cd9e8b53

doc(tactic/core,uniform_space/basic): minor doc fixes (#3115)

robertylewis committed 5 years ago

103743e3

feat(algebra/big_operators): `prod_apply_dite` and `prod_dite` (#3110)

Vierkantor committed 5 years ago

8e44b9f1

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

leanprover-community-bot committed 5 years ago

56a580d2

chore(*): regularize naming using injective (#3071)

kim-em committed 5 years ago

ed44541a

feat(category_theory/discrete): build equivalence from equiv (#3099)

kim-em committed 5 years ago

e060c93d

perf(tactic/linarith): implement redundancy test to reduce number of comparisons (#3079)

robertylewis committed 5 years ago

73caeaa5

refactor(category_theory/abelian): use has_finite_products (#2917)

kim-em committed 5 years ago

21bf8737

chore(*): update to lean 3.16.3 (#3107)

kim-em committed 5 years ago

53af7145

chore(data/finset): minor review (#3105)

urkud committed 5 years ago

24792be6

fix(tactic/linarith): don't fail trying to preprocess irrelevant hypotheses (#3104)

robertylewis committed 5 years ago

eb5b7fb7

chore(category_theory/closed/cartesian): style (#3098)

kim-em committed 5 years ago

b91909e7

feat(algebra/linear_ordered_comm_group_with_zero) define linear_ordered_comm_group_with_zero (#3072)

kckennylau committed 5 years ago

b5baf555

refactor(measure_theory): make `volume` a bundled measure (#3075)

urkud committed 5 years ago

48c4f400

Newer Older