leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into eric-wieser/bochner-generalizations

eric-wieser committed 2 years ago

44430d01

feat (analysis/mellin_transform): API for mellin transforms (#19110)

loefflerd committed 2 years ago

917c3c07

chore(analysis/calculus/deriv): split file (#19113)

urkud committed 2 years ago

3bce8d80

feat(measure_theory/function/l1_space): generalize multiplicative results to is_unit (#19073)

eric-wieser committed 2 years ago

13b0d72f

chore(measure_theory/function/simple_func_dense_lp): generalize typeclasses (#19111)

eric-wieser committed 2 years ago

5a2df4cd

chore(*): add mathlib4 synchronization comments (#19099)

leanprover-community-bot committed 2 years ago

0b7c740e

refactor(measure_theory/function/lp_space): split file (#19112)

eric-wieser committed 2 years ago

c4015acc

feat(linear_algebra/alternating): add 3 missing definitions (#19069)

urkud committed 2 years ago

78fdf68d

feat (measure_theory/integral): some simple substitution rules (#19106)

loefflerd committed 2 years ago

b84aee74

feat(number_theory/class_number/finite): remove useless assumption [dedekind_domain R] (#19109)

faenuccio committed 2 years ago

ea0bcd84

Generalize a bunch of downstream file too

eric-wieser committed 2 years ago

a9618136

generalize the rest

eric-wieser committed 2 years ago

a3cee72d

Merge remote-tracking branch 'origin/staging' into eric-wieser/bounded-smul-cleanup

eric-wieser committed 2 years ago

dfd463de

fix: missing continuity attribute (#19104)

eric-wieser committed 2 years ago

62748956

feat(analysis/convex/gauge): gauge of a convex nhd of zero is continuous (#19102)

urkud committed 2 years ago

373b03b5

refactor(measure_theory/function/lp_space): generalize actions from `normed_field` to `normed_ring` (#19083)

eric-wieser committed 2 years ago

e0736bb5

feat(data/set/finite): add a version of `set.finite.bUnion` (#19098)

urkud committed 2 years ago

5bb9fffd

feat(analysis/inner_product_space/spectrum): add a decomposition instance (#14870)

eric-wieser committed 2 years ago

a33d01f7

feat(topology/subset_properties): add `sigma_compact_space` instances (#19100)

urkud committed 2 years ago

76f9c990

feat(analysis/calculus/bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097)

urkud committed 2 years ago

42e9a1fd

chore(topology/continuous_function/ideals): generalize type class requirements (#19093)

j-loreaux committed 2 years ago

c2258f7b

chore(measure_theory/function/lp_space): add and reorder monotonicity results (#19092)

eric-wieser committed 2 years ago

d2d14e72

feat(data/real/basic): add `real.supr_nonneg` etc (#19096)

urkud committed 2 years ago

cb425931

feat(topology/{maps,separation}): add lemmas about closed and quotient maps (#19071)

urkud committed 2 years ago

d91e7f7a

doc(analysis/complex/arg): fix docs (#19095)

ericrbg committed 2 years ago

45a46f4f

feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062)

eric-wieser committed 2 years ago

e1a18cad

feat(algebra/homology/local_cohomology): just the definition (#19061)

emwitt committed 2 years ago

5a684ce8

feat(analysis/normed_space/lp_space): generalize from normed_field to `normed_ring` (#19085)

eric-wieser committed 2 years ago

de83b437

chore(measure_theory/function/lp_space): add nnnorm lemmas (#19091)

eric-wieser committed 2 years ago

6480bedf

chore(*): add mathlib4 synchronization comments (#19089)

leanprover-community-bot committed 2 years ago

a87d2257

Older