leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 2 years ago

0c0dadf8

chore(analysis/inner_product_space/pi_L2): euclidean space is a real inner product space

eric-wieser committed 2 years ago

e4d0b0e9

chore(analysis/normed_space/pi_Lp): missing scalar tower instances (#18577)

eric-wieser committed 2 years ago

2fd0de23

refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_like instances (#18575)

eric-wieser committed 2 years ago

bd1fc183

refactor(algebra/group/basic): rework lemmas on inv and neg (#17483)

MichaelStollBayreuth committed 2 years ago

2196ab36

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

leanprover-community-bot committed 2 years ago

69c6a5a1

chore(number_theory/pell_matiyasevic): generalize `is_pell` to arbitary `d` (#18573)

eric-wieser committed 2 years ago

795b5018

feat(analysis/normed_space/*exponential): more results about `star` (#18553)

eric-wieser committed 2 years ago

1e320130

refactor(number_theory/zsqrtd): replace `zsqrtd.conj` with `star` (#18572)

eric-wieser committed 2 years ago

2af08364

chore(topology/order/basic): generalise frontier_Icc (#18571)

ericrbg committed 2 years ago

c985ae98

chore(data/finset/locally_finite): lemmas about open intervals (#18533)

eric-wieser committed 2 years ago

f24cc289

refactor(*): reduce dependencies on ring_theory.ideal.quotient_operations (#18530)

jcommelin committed 2 years ago

da420a8c

feat(probability/kernel/composition): composition of kernels (#17974)

RemyDegenne committed 2 years ago

3180fab6

feat(probability/probability_mass_function): basic lawful monad lemmas for `pmf`. (#18469)

dtumad committed 2 years ago

4ac69b29

feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680)

fpvandoorn committed 2 years ago

ddec54a7

feat(number_theory/pell): add exists_pos_of_not_is_square (#18567)

MichaelStollBayreuth committed 2 years ago

5b05c634

chore(data/matrix/basic): add a star_module instance (#18557)

eric-wieser committed 2 years ago

21e3562c

chore(data/matrix/basic): generalize an instance (#18563)

eric-wieser committed 2 years ago

d23150d1

feat(algebra/star/self_adjoint): add and generalize trivial lemmas (#18558)

eric-wieser committed 2 years ago

671d5d9a

chore(topology/instances/ennreal): drop a dependency (#18562)

urkud committed 2 years ago

90ac7a91

chore(category_theory/sites/pushforward): move pushforwards to own file to reduce imports (#18561)

kim-em committed 2 years ago

e2e38c00

chore(topology/algebra/with_zero_topology): move to a new NS, used `localized` (#18560)

urkud committed 2 years ago

3e0c4d76

chore(category_theory/preadditive): reduce unnecessary imports (#18559)

kim-em committed 2 years ago

09f981f7

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

leanprover-community-bot committed 2 years ago

f4758115

feat(analysis/fourier): Poisson summation for polynomially-decaying functions (#18556)

loefflerd committed 2 years ago

38f16f96

feat(geometry/manifold/vector_bundle/basic): smooth vector bundles (#17611)

hrmacbeth committed 2 years ago

be2c24f5

chore(linear_algebra/affine_space/midpoint): factor out lemmas about char_zero (#18555)

mcdoll committed 2 years ago

78261225

feat(topology/homeomorph): add `homeomorph.symm_symm` (#18551)

urkud committed 2 years ago

3b267e70

feat(measure_theory/function/l1_space): Hölder's inequality specialized to integrable functions (#18550)

hrmacbeth committed 2 years ago

346bace1

feat(measure_theory/integral): integral_tsum (#18549)

hrmacbeth committed 2 years ago

fbde2f60

Older