Commits leanprover-community/mathlib

feat(algebra/char_p/basic): refactor proof of add_pow_char_of_commute to extract a statement true in all rings (#11364)

alexjbest committed 3 years ago

ceb887dd

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

eric-wieser committed 3 years ago

2fd0de23

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

eric-wieser committed 3 years ago

bd1fc183

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

MichaelStollBayreuth committed 3 years ago

2196ab36

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

github-actions[bot] committed 3 years ago

69c6a5a1

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

eric-wieser committed 3 years ago

795b5018

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

eric-wieser committed 3 years ago

1e320130

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

eric-wieser committed 3 years ago

2af08364

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

ericrbg committed 3 years ago

c985ae98

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

eric-wieser committed 3 years ago

f24cc289

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

jcommelin committed 3 years ago

da420a8c

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

RemyDegenne committed 3 years ago

3180fab6

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

dtumad committed 3 years ago

4ac69b29

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

fpvandoorn committed 3 years ago

ddec54a7

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

MichaelStollBayreuth committed 3 years ago

5b05c634

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

eric-wieser committed 3 years ago

21e3562c

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

eric-wieser committed 3 years ago

d23150d1

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

eric-wieser committed 3 years ago

671d5d9a

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

urkud committed 3 years ago

90ac7a91

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

kim-em committed 3 years ago

e2e38c00

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

urkud committed 3 years ago

3e0c4d76

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

kim-em committed 3 years ago

09f981f7

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

github-actions[bot] committed 3 years ago

f4758115

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

loefflerd committed 3 years ago

38f16f96

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

hrmacbeth committed 3 years ago

be2c24f5

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

mcdoll committed 3 years ago

78261225

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

urkud committed 3 years ago

3b267e70

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

hrmacbeth committed 3 years ago

346bace1

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

hrmacbeth committed 3 years ago

fbde2f60

feat(number_theory/number_field/basic): add integral_basis (#18474)

xroblot committed 3 years ago

641b6a82