leanprover-community/mathlib

Pull Requests Commits

feat(analysis/normed_space/multilinear): a few more bundled (bi)linear maps (#6546)

urkud committed 5 years ago

ebe2c616

feat(analysis/special_functions/integrals): mul/div by a const (#6357)

benjamindavidson committed 5 years ago

9f17db51

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

leanprover-community-bot committed 5 years ago

07fc9821

refactor(data/{finset,multiset}): move inductions proofs on sum/prod from finset to multiset, add more induction lemmas (#6561)

RemyDegenne committed 5 years ago

df1e6f92

feat(data/set/basic): add `set.set_ite` (#6557)

urkud committed 5 years ago

b280b005

chore(geometry/manifold): use `namespace`, rename `image` to `image_eq` (#6517)

urkud committed 5 years ago

ac8a1196

feat(order/filter/*, topology/subset_properties): define "coproduct" of two filters (#6372)

hrmacbeth committed 5 years ago

16ef2913

feat(topology/paracompact): define paracompact spaces (#6395)

urkud committed 5 years ago

0fa0d61e

feat(data/real/nnreal): ℝ is an ℝ≥0-algebra (#6560)

adomani committed 5 years ago

126cebca

doc(*): wrap raw URLs containing parentheses with angle brackets (#6554)

bryangingechen committed 5 years ago

a05b35ca

feat(category_theory/opposites): use simps everywhere (#6553)

fpvandoorn committed 5 years ago

3e5643e8

feat(algebra/ring/boolean_ring): Boolean rings (#6464)

bryangingechen committed 5 years ago

5962c76f

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

leanprover-community-bot committed 5 years ago

32547fc8

chore(polynomial/chebyshev): changes names of chebyshev₁ to chebyshev.T and chebyshev₂ to chebyshev.U (#6519)

Julian-Kuelshammer committed 5 years ago

44282437

feat(topology/local_homeomorph): preimage of `closure` and `frontier` (#6547)

urkud committed 5 years ago

4bc67070

feat(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) (#6520)

awainverse committed 5 years ago

cbcbe24d

feat(data/polynomial/mirror): new file (#6426)

tb65536 committed 5 years ago

626cb422

feat(group_theory/subgroup): add monoid_hom.restrict (#6537)

kex-y committed 5 years ago

913950ed

feat(measure_theory/[set_integral, interval_integral]): mono and nonneg lemmas (#6292)

ADedecker committed 5 years ago

d40487b5

Make *_*_iff argument implicit

gebner committed 5 years ago

5d526637

gebner committed 5 years ago

872cc71c

feat(algebra/lie/subalgebra): define the Lie subalgebra generated by a subset (#6549)

ocfnash committed 5 years ago

97d13d75

chore(linear_algebra/*): changes to finsupp_vectorspaces and move module doc dual (#6516)

Julian-Kuelshammer committed 5 years ago

d90448c6

chore(analysis/normed_space/units): add `protected`, minor review (#6544)

urkud committed 5 years ago

c782e282

feat(data/mv_polynomial/basic): add is_scalar_tower and smul_comm_class instances (#6542)

eric-wieser committed 5 years ago

f158f25d

fix(*): remove some simp lemmas (#6541)

fpvandoorn committed 5 years ago

340dd69f

chore(analysis/normed_space/extend): remove unnecessary imports (#6538)

hrmacbeth committed 5 years ago

990a5bbd

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

leanprover-community-bot committed 5 years ago

10aadddf

chore(algebra/algebra/basic): add a missing coe lemma (#6535)

eric-wieser committed 5 years ago

d2cc044f

feat(data/finsupp, algebra/monoid_algebra): add is_scalar_tower and smul_comm_class (#6534)

eric-wieser committed 5 years ago

ef1a00b6

Newer Older