leanprover-community/mathlib3

Pull Requests Commits

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

Remove dead code

ADedecker committed 4 years ago

d389964a

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

b-mehta committed 4 years ago

afd0f92b

Merge branch 'monotone_integrable' of https://github.com/leanprover-community/mathlib into monotone_integrable

ADedecker committed 4 years ago

03eac2bd

ADedecker committed 4 years ago

7edac7d0

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

Merge branch 'master' into monotone_integrable

ADedecker committed 4 years ago

Verified 3149abf2

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

hrmacbeth committed 4 years ago

02ecb62a

Merge branch 'monotone_measurable_subset' into monotone_integrable

ADedecker committed 4 years ago

2ff1e688

Merge remote-tracking branch 'origin/master' into monotone_integrable

ADedecker committed 4 years ago

03f5f86f

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

Generalize monotone.measurable to monotone on set

ADedecker committed 4 years ago

d656bf01

Remove useless set instance

ADedecker committed 4 years ago

2f07ced3

ADedecker committed 4 years ago

cf6d668b

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

Newer Older