leanprover-community/mathlib

Pull Requests Commits

AlexKontorovich committed 4 years ago

b0988c53

AlexKontorovich committed 4 years ago

fdbfe76c

AlexKontorovich committed 4 years ago

e1199138

AlexKontorovich committed 4 years ago

3d667a2f

nothing particularly useful

hrmacbeth committed 4 years ago

7291cf3c

covers work (incomplete)

AlexKontorovich committed 4 years ago

0cfccd34

averaging almost done

AlexKontorovich committed 4 years ago

040a2f5c

AlexKontorovich committed 4 years ago

d053be87

hrmacbeth committed 5 years ago

fe01d6af

box_integral stuff

AlexKontorovich committed 5 years ago

4615add1

fix lemma naming

hrmacbeth committed 5 years ago

ceff4110

reframe line additivity to lower dimension

hrmacbeth committed 5 years ago

bd7af8ef

hrmacbeth committed 5 years ago

4890abea

additivity facts

hrmacbeth committed 5 years ago

12bbdf8f

box_line_integral_linear

AlexKontorovich committed 5 years ago

38263605

AlexKontorovich committed 5 years ago

83784cf6

box_line_int done

AlexKontorovich committed 5 years ago

3468f4df

hrmacbeth committed 5 years ago

0cd35900

redefine rectangles

hrmacbeth committed 5 years ago

30c2947d

continuous implies integrable

hrmacbeth committed 5 years ago

43182dc6

AlexKontorovich committed 5 years ago

48f1db3a

box additive lemmas

AlexKontorovich committed 5 years ago

c7ff76cf

sketch out additivity of integration; messy code

hrmacbeth committed 5 years ago

76558cd2

AlexKontorovich committed 5 years ago

9d4f02dc

additivity of line integrals

hrmacbeth committed 5 years ago

f03d1ef7

Update src/analysis/normed_space/box_subadditive.lean

urkud committed 5 years ago

Verified ee354e62

Merge branch 'master' into box-subadditive

urkud committed 5 years ago

c91bccea

feat(category_theory/limits): Any small complete category is a preorder (#4907)

b-mehta committed 5 years ago

246df99f

feat(category_theory/limits/presheaf): left adjoint if preserves colimits (#4896)

b-mehta committed 5 years ago

40245977

chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888)

eric-wieser committed 5 years ago

6a1ce57b

Older