leanprover-community/mathlib

Pull Requests Commits

feat (number_theory/zeta_function): define zeta (#19027)

loefflerd committed 2 years ago

a8410892

feat(analysis/schwartz_space): partial derivatives (#18755)

mcdoll committed 2 years ago

e3e30a5c

feat(analysis/normed_space/triv_sq_zero_ext): generalize some results to non-commutativity (#19049)

eric-wieser committed 2 years ago

88a563b1

fix(scripts): Allow special character in file names (#11001)

eric-wieser committed 2 years ago

7bf0850d

chore(ring_theory/adjoin_root): modify `field` instance on `adjoin_root` (#19119)

adomani committed 2 years ago

5c4b3d41

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

hrmacbeth committed 2 years ago

f7ebde7e

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

Multramate committed 2 years ago

d87199d5

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

Multramate committed 2 years ago

4f840b8d

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

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

Newer Older