Commits leanprover-community/mathlib3

Merge remote-tracking branch 'origin/eric-wieser/trivial-basis.parallelepiped-lemmas' into eric-wieser/parallelepiped-extras

eric-wieser committed 2 years ago

df54a6c6

Merge remote-tracking branch 'origin/master' into eric-wieser/trivial-basis.parallelepiped-lemmas

eric-wieser committed 2 years ago

f8ab07ba

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

leanprover-community-bot committed 2 years ago

bd15ff41

chore(measure_theory/measure/outer_measure): lemmas about zero and top (#18983)

eric-wieser committed 2 years ago

343e8020

feat(ring_theory/polynomial): show gaussian form of `hermite n` (#18896)

jakelev committed 2 years ago

066ecdb4

feat(analysis/mellin_transform): Mellin transforms (#18822)

loefflerd committed 2 years ago

9e6d4aec

chore(algebra/order/group/defs): remove some instances that cause timeouts with etaExperiment (#18985)

kim-em committed 2 years ago

b599f4e4

feat(topology/sets/compacts): add `positive_compacts.map` (#18872)

eric-wieser committed 2 years ago

8c1b484d

chore(probability/independence): create independence folder, split old file into two parts (#18987)

RemyDegenne committed 2 years ago

2f834701

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

leanprover-community-bot committed 2 years ago

781cb2ee

feat(analysis/normed/order/lattice): add has_solid_norm (#18554)

xroblot committed 2 years ago

5dc275ec

chore(topology/instances/ennreal): missing smul lemmas (#18980)

eric-wieser committed 2 years ago

ec4b2eeb

feat(data/finset/lattice): Distributivity lemmas (#18611)

YaelDillies committed 2 years ago

2d44d682

feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743)

eric-wieser committed 2 years ago

213b0cff

feat(probability/kernel/measurable_integral): the integral against a kernel is strongly measurable (#18974)

RemyDegenne committed 2 years ago

28b2a92f

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

leanprover-community-bot committed 2 years ago

a2706b55

feat(number_theory/diophantine_approximation): add Legendre's thm on rat'l approximations (#18460)

MichaelStollBayreuth committed 2 years ago

e25a3174

refactor(algebra): Redefine `a ≡ b [PMOD p]` (#18958)

YaelDillies committed 2 years ago

a07d7509

feat(number_theory/pell): add def and properties of fundamental solutions (#18901)

MichaelStollBayreuth committed 2 years ago

0b20dffb

chore(algebra/order/absolute_value): remove unneeded imports (#18978)

kim-em committed 2 years ago

0013240b

chore(representation_theory/group_cohomology): use `fin.cast_succ` instead of coe (#18950)

eric-wieser committed 2 years ago

cc5dd624

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

leanprover-community-bot committed 2 years ago

7d34004e

feat(*): generalise+add algebraic instances (#18947)

ericrbg committed 2 years ago

949dc57e

feat(data/real/ennreal): interactions between infi/supr and to_nnreal/to_real (#18946)

collares committed 2 years ago

c1686dff

feat(field_theory/adjoin,normal): `field_range` lemmas (#18959)

tb65536 committed 2 years ago

d4437c68

feat(field_theory/intermediate_field): Inhabited instance (#18956)

tb65536 committed 2 years ago

c596622f

feat(probability/kernel/basic): integrals of basic kernels (#18961)

RemyDegenne committed 2 years ago

a9545e8a

feat(probability/kernel/basic): add `kernel.comap_right` and `kernel.piecewise` (#18917)

RemyDegenne committed 2 years ago

63decdb8

feat(algebra/order/group/order_iso): add `order_iso.div_{left,right}` (#18968)

urkud committed 2 years ago

6632ca20

feat(analysis/calculus/deriv): `polynomial.aeval` lemmas (#18945)

eric-wieser committed 2 years ago

f81174bd