leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 4 years ago

Verified 22fc5626

feat(combinatorics/simple_graph): `boolean_algebra` for `simple_graph`s. (#8330)

ericrbg committed 4 years ago

28b85931

refactor(measure_theory/decomposition): move `decomposition` into a folder (#8374)

kex-y committed 4 years ago

fb58e059

feat(combinatorics/colex): top of the colex ordering on finite types (#8379)

b-mehta committed 4 years ago

b45acc9c

feat(analysis/normed_space): Define conformal maps on inner product spaces; define the groupoid of conformal maps (#8367)

justadzr committed 4 years ago

02a56964

feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375)

Vierkantor committed 4 years ago

899bb5f9

feat(data/sym2): add the universal property, and make `sym2.is_diag ⟦(x, y)⟧ ↔ x = y` true definitionally (#8358)

eric-wieser committed 4 years ago

4676b31f

feat(combinatorics/colex): golf and generalise (#8301)

b-mehta committed 4 years ago

6ac3059b

fix(data/matrix/basic): remove an accidental requirement for a matrix to be square (#8372)

l534zhan committed 4 years ago

ed8d597a

feat(ring_theory): define `fractional_ideal.adjoin_integral` (#8296)

Vierkantor committed 4 years ago

fce38f1a

feat(group_theory/order_of_element): pow_eq_mod_card (#8354)

ChrisHughes24 committed 4 years ago

c05c15fe

feat(measure_theory/borel_space): generalize `monotone.measurable` to monotone on set (#8365)

ADedecker committed 4 years ago

0f9b754f

feat(topology/continuous_function/bounded): prove `norm_eq_supr_norm` (#8288)

ocfnash committed 4 years ago

15893184

feat(measure_theory/vector_measure): introduce vector-valued measures (#8247)

kex-y committed 4 years ago

f5d25b48

chore(topology/continuous_function, analysis/normed_space): use `is_empty α` instead of `¬nonempty α` (#8352)

eric-wieser committed 4 years ago

0f58e131

chore(.docker): add missing library (#8370)

kim-em committed 4 years ago

b3fbcec6

feat(algebra.homology): homology f g w ≅ cokernel (kernel.lift g f w) (#8355)

kim-em committed 4 years ago

e0467bd0

feat(analysis/convex): convex sets with zero (#8234)

b-mehta committed 4 years ago

11af02c3

feat(category_theory/limits): strict initial objects (#8094)

b-mehta committed 4 years ago

0821e6ed

feat(category_theory/limits/pullbacks): generalise pullback mono lemmas (#8302)

b-mehta committed 4 years ago

afd0f92b

chore(.gitignore): ignore lock files (#8368)

alexjbest committed 4 years ago

739b353d

feat(linear_algebra/finsupp): `span.repr` gives an arbitrarily representation of `x : span R w` as a linear combination over `w` (#8339)

kim-em committed 4 years ago

ad7ab8d8

feat(analysis/fourier): span of monomials is dense in L^p (#8328)

hrmacbeth committed 4 years ago

02ecb62a

feat(topology/metric_space/basic): an order-bounded set is metric-bounded (#8335)

ADedecker committed 4 years ago

5ccf2bf2

feat(topology/algebra/ordered): an `order_closed_topology` restricted to a subset is an `order_closed_topology` (#8364)

ADedecker committed 4 years ago

3e679326

chore(order/basic): whitespaces and caps (#8359)

YaelDillies committed 4 years ago

dd9f1c3b

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

leanprover-community-bot committed 4 years ago

6a20dd63

feat(data/finset/basic): product, bUnion, sdiff lemmas (#8321)

YaelDillies committed 4 years ago

ee607111

chore(analysis/*): remove unnecessary imports (#8344)

YaelDillies committed 4 years ago

c2d042c6

feat(measure_theory): add lemmas of equality of measures under assumptions of null difference, in particular null frontier (#8332)

kkytola committed 4 years ago

b02b9197

Older