Commits leanprover-community/mathlib

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

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

xroblot committed 2 years ago

641b6a82

chore(logic/equiv/basic): Generalize Type to Sort (#18543)

eric-wieser committed 2 years ago

d2d8742b

fix(data/set/semiring): fix lemma name (#18545)

eric-wieser committed 2 years ago

62e8311c

feat(field_theory/ratfunc): add lemma `coe_sub` (#18542)

faenuccio committed 2 years ago

ec80bb15

feat(ring_theory/hahn_series): add lemma neg_order (#18541)

faenuccio committed 2 years ago

a484a7d0

chore(algebra/algebra/restrict_scalars): replace `restrict_scalars_smul_def` with version that does not commit defeq-abuse. (#18540)

ocfnash committed 2 years ago

c310cfdc

fix(algebra/algebra/operations): add missing `set_semiring.down` casts (#18539)

eric-wieser committed 2 years ago

27b54c47

chore(ring_theory/finiteness): remove references to `ideal.quotient` (#18538)

jcommelin committed 2 years ago

f5edf469

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

leanprover-community-bot committed 2 years ago

832f7b91

feat(linear_algebra/free_module/pid): rename module.free_of_finite_type_torsion_free (#18537)

xroblot committed 2 years ago

f62c15c0

refactor(topology/algebra/field): drop `topological_space_units` (#18536)

urkud committed 2 years ago

c10e724b

chore(set_theory/ordinal/initial_seg): swap the names of `init` and `init'` (#18534)

astrainfinita committed 2 years ago

8da9e305

feat(linear_algebra/direct_sum/tensor_product): one-sided distributivity constructions (#18514)

eric-wieser committed 2 years ago

9b9d125b

refactor(ring_theory/ideal/operations): split quotients to a new file (#18531)

jcommelin committed 2 years ago

e7f0ddbf

chore(topology/algebra/ring): split into 2 files (#18532)

urkud committed 2 years ago

9a59dcb7

feat(data.polynomial.div): add `theorem X_pow_dvd_iff` (#18528)

faenuccio committed 2 years ago

742aa2cb

feat(analysis/complex/upper_half_plane/metric): prove that SL(2, ℝ) acts isometrically on upper half space with the hyperbolic metric (#18379)

RuizheWan committed 2 years ago

f06058e6