leanprover-community/mathlib

Pull Requests Commits

chore(algebra/ring,char_zero): generalize some lemmas (#3141)

urkud committed 6 years ago

23d61413

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

leanprover-community-bot committed 6 years ago

52abfcf5

feat(data/finset): add card_insert_of_mem (#3137)

kbuzzard committed 6 years ago

b5625759

chore(*): update to Lean 3.16.4c (#3139)

robertylewis committed 6 years ago

36e3b9f1

feat(order/complete_lattice): complete lattice of Sup (#3138)

b-mehta committed 6 years ago

67844a81

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

urkud committed 6 years ago

f0593365

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

jsm28 committed 6 years ago

54cc126b

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

hrmacbeth committed 6 years ago

86dcd5cd

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

jsm28 committed 6 years ago

46a88944

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

kckennylau committed 6 years ago

105fa176

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

bryangingechen committed 6 years ago

068aaafa

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

kbuzzard committed 6 years ago

3f9b52ae

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

leanprover-community-bot committed 6 years ago

6aba9580

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

bryangingechen committed 6 years ago

d59adc18

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

robertylewis committed 6 years ago

5b5ff790

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

PatrickMassot committed 6 years ago

eff9ed3a

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

robertylewis committed 6 years ago

7073c8b9

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

robertylewis committed 6 years ago

b7d056a1

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

robertylewis committed 6 years ago

d097161b

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

cipher1024 committed 6 years ago

8729fe21

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

PatrickMassot committed 6 years ago

e8ff6ff6

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

alexjbest committed 6 years ago

cd9e8b53

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

robertylewis committed 6 years ago

103743e3

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

Vierkantor committed 6 years ago

8e44b9f1

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

leanprover-community-bot committed 6 years ago

56a580d2

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

kim-em committed 6 years ago

ed44541a

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

kim-em committed 6 years ago

e060c93d

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

robertylewis committed 6 years ago

73caeaa5

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

kim-em committed 6 years ago

21bf8737

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

kim-em committed 6 years ago

53af7145

Newer Older