leanprover-community/mathlib3

Pull Requests Commits

feat(data/set/ncard): noncomputable set cardinality (#18576)

apnelson1 committed 2 years ago

74c2af38

refactor(analysis/calculus/darboux): review API (#19125)

urkud committed 2 years ago

9a1ffe49

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

leanprover-community-bot committed 2 years ago

f60c6087

chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123)

urkud committed 2 years ago

bd654783

chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)

eric-wieser committed 2 years ago

837f72de

doc(topology/homotopy/H-spaces): add doc about H-spaces. (#19075)

faenuccio committed 2 years ago

729d23f9

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

Newer Older