leanprover-community/mathlib3

Pull Requests Commits

refactor(topology/vector_bundle/hom): fibres of hom-bundle carry strong topology (#19107)

hrmacbeth committed 3 years ago

f7ebde7e

feat(linear_algebra/free_module/ideal_quotient): add ideal.finrank_quotient_eq_sum (#19084)

Multramate committed 3 years ago

d87199d5

feat(ring_theory/polynomial/quotient): generalise quotient_span_X_sub_C_alg_equiv (#19086)

Multramate committed 3 years ago

4f840b8d

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

loefflerd committed 3 years ago

917c3c07

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

urkud committed 3 years ago

3bce8d80

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

eric-wieser committed 3 years ago

13b0d72f

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

eric-wieser committed 3 years ago

5a2df4cd

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

github-actions[bot] committed 3 years ago

0b7c740e

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

eric-wieser committed 3 years ago

c4015acc

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

urkud committed 3 years ago

78fdf68d

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

loefflerd committed 3 years ago

b84aee74

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

faenuccio committed 3 years ago

ea0bcd84

fix: missing continuity attribute (#19104)

eric-wieser committed 3 years ago

62748956

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

urkud committed 3 years ago

373b03b5

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

eric-wieser committed 3 years ago

e0736bb5

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

urkud committed 3 years ago

5bb9fffd

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

eric-wieser committed 3 years ago

a33d01f7

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

urkud committed 3 years ago

76f9c990

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

urkud committed 3 years ago

42e9a1fd

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

j-loreaux committed 3 years ago

c2258f7b

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

eric-wieser committed 3 years ago

d2d14e72

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

urkud committed 3 years ago

cb425931

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

urkud committed 3 years ago

d91e7f7a

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

ericrbg committed 3 years ago

45a46f4f

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

eric-wieser committed 3 years ago

e1a18cad

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

emwitt committed 3 years ago

5a684ce8

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

eric-wieser committed 3 years ago

de83b437

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

eric-wieser committed 3 years ago

6480bedf

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

github-actions[bot] committed 3 years ago

a87d2257

feat(linear_algebra/span): generalise to_span_nonzero_singleton (#19082)

Multramate committed 3 years ago

10878f6b

Newer Older