leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 2 years ago

44d30385

Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-exp-properties-2

eric-wieser committed 2 years ago

f6114856

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

eric-wieser committed 2 years ago

05c93649

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

MichaelStollBayreuth committed 2 years ago

5b05c634

Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-exp-properties-2

eric-wieser committed 2 years ago

ef6ce267

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

eric-wieser committed 2 years ago

4b90d051

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

mcdoll committed 2 years ago

78261225

feat(analysis/normed_space/matrix_exponential): symmetry and conjugate symmetry

eric-wieser committed 2 years ago

fc838103

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

Older