leanprover-community/mathlib

Pull Requests Commits

chore(logic/function): `simp`lify applications of `(un)curry` (#4696)

urkud committed 5 years ago

0523b61d

Revert "chore(data/multiset): add a few lemmas"

urkud committed 5 years ago

a1f17706

chore(data/multiset): add a few lemmas

urkud committed 5 years ago

45caa4f3

fix(tactic/norm_num): remove unnecessary argument to rat.cast_zero (#4682)

bryangingechen committed 5 years ago

cacc297c

feat(ring_theory/witt_vector/structure_polynomial): examples and basic properties (#4467)

jcommelin committed 5 years ago

0f1bc68f

feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363)

kim-em committed 5 years ago

4140f789

feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `linear_map.to_matrix` (#4650)

Vierkantor committed 5 years ago

ef9d00f7

feat(data/complex/exponential): bounds on exp (#4432)

jsm28 committed 5 years ago

47dcecd2

feat(ring_theory/polynomial/chebyshev): chebyshev polynomials of the first kind (#4267)

jcommelin committed 5 years ago

c38d128c

feat(algebra/*): some simp lemmas, and changing binders (#4681)

kim-em committed 5 years ago

f75dbd3d

feat(algebra/infinite_sum): make tsum irreducible (#4679)

fpvandoorn committed 5 years ago

41c227a1

feat(ring_theory/adjoin): adjoin_singleton_one (#4633)

jcommelin committed 5 years ago

7601a7a5

feat(*): make int.nonneg irreducible (#4601)

sgouezel committed 5 years ago

4b890a24

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

leanprover-community-bot committed 5 years ago

d174295c

fix(data/equiv): nolint typo (#4677)

fpvandoorn committed 5 years ago

9d1bbd10

refactor(tactic/norm_num): define prove_ne_zero using prove_ne (#4626)

digama0 committed 5 years ago

49bb5dd9

fix(logic/nontrivial): change tactic doc entry tag to more common "type class" (#4676)

bryangingechen committed 5 years ago

1ac5d822

chore(linear_algebra/affine_space): introduce notation for `affine_map` (#4675)

urkud committed 5 years ago

61e1111d

chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672)

urkud committed 5 years ago

4faf2e21

chore(order/filter): run `dsimp only [set.mem_set_of_eq]` in `filter_upwards` (#4671)

urkud committed 5 years ago

392d52c2

feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} (#4595)

jcommelin committed 5 years ago

93b7e635

chore(analysis/calculus/fderiv): golf a lemma using new `nontriviality` (#4584)

urkud committed 5 years ago

fee2dfaa

feat(topology/subset_properties): define `filter.cocompact` (#4666)

urkud committed 5 years ago

e21dc7a9

chore(analysis/normed_space/basic): add `continuous_at.inv'`, `continuous.div` etc (#4667)

urkud committed 5 years ago

cc32876d

feat(measure_theory/prod): product measures and Fubini's theorem (#4590)

fpvandoorn committed 5 years ago

db06b677

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

leanprover-community-bot committed 5 years ago

c7782bb1

chore(data/set/intervals): more lemmas (#4662)

urkud committed 5 years ago

77dc6794

chore(order/filter): add a few lemmas (#4661)

urkud committed 5 years ago

95852107

chore(data/finsupp/basic): rename type variables (#4624)

urkud committed 5 years ago

f9908388

feat(logic/nontrivial): make `nontriviality` work for more goals (#4574)

urkud committed 5 years ago

ebd2b7f2

Newer Older