leanprover-community/mathlib3

Pull Requests Commits

feat(measure_theory/integral/average): FIrst moment method for the Lebesgue integral

YaelDillies committed 2 years ago

9c3d3d9b

YaelDillies committed 2 years ago

13b28337

YaelDillies committed 2 years ago

daa244d2

Merge remote-tracking branch 'origin/master' into first_moment

YaelDillies committed 2 years ago

0231ed13

chore(measure_theory/function/ess_sup): Generalise (#18669)

YaelDillies committed 2 years ago

52932b3a

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

leanprover-community-bot committed 2 years ago

86d1873c

feat(linear_algebra/matrix/nonsingular_inverse): decomposition of block matrices with an invertible corner (#18847)

eric-wieser committed 2 years ago

e49764de

feat(data/matrix/basic): miscellaneous defs and lemmas (#8289)

YaelDillies committed 2 years ago

eba5bb31

feat(order/monotone/basic): `function.update` is monotone (#18841)

YaelDillies committed 2 years ago

90df25de

fix(group_theory/monoid_localization): fix timeout (#18846)

eric-wieser committed 2 years ago

10ee9413

feat(order/compactly_generated): For any `b`, there exists a set of independent atoms `s` such that `Sup s` is the complement of `b`. (#8475)

winston-h-zhang committed 2 years ago

e8cf0cfe

feat(algebra/group_with_zero): add lemmas about `f * pi.single i x` (#6418)

urkud committed 2 years ago

246f6f79

feat(linear_algebra/matrix/nonsingular_inverse): interchange of matrix reindexing and inversion (#18812)

MohanadAhmed committed 2 years ago

996a8530

feat(algebra/order/ring/defs): negative versions of order lemmas (#18831)

eric-wieser committed 2 years ago

44e29dbc

feat(linear_algebra/tensor_product/matrix): connect with `matrix.kronecker` (#18616)

eric-wieser committed 2 years ago

f784cc61

feat(order/directed): Scott continuous functions (#18517)

mans0954 committed 2 years ago

485b24ed

feat(data/set/intervals/unordered_interval): `prod` and `pi` lemmas (#18835)

eric-wieser committed 2 years ago

4020ddee

refactor(algebra/module/dedekind_domain): eliminate existentials (#14734)

eric-wieser committed 2 years ago

cdc34484

feat(data/finset/basic): `insert` and `erase` lemmas (#18729)

YaelDillies committed 2 years ago

9ac7c0c8

feat(group_theory/monoid_localization): Order (#18724)

YaelDillies committed 2 years ago

13b8e258

chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749)

vihdzp committed 2 years ago

730c6d4c

feat(data/matrix/rank): rank of `Aᵀ ⬝ A` and `Aᴴ ⬝ A` (#18818)

eric-wieser committed 2 years ago

17219820

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

leanprover-community-bot committed 2 years ago

8eb9c42d

feat(ring_theory/polynomial): define the probabilist's Hermite polynomials (#18739)

lukemantle committed 2 years ago

c6275ef4

chore(data/complex/module): split out orientation to a separate file (#18824)

kim-em committed 2 years ago

cd8fafa2

chore(linear_algebra/matrix/basis): reduce imports (#18823)

kim-em committed 2 years ago

6c263e4b

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

leanprover-community-bot committed 2 years ago

ce38d86c

feat(topology/perfect): Schemes, embedding of the Cantor space (#18248)

Felix-Weilacher committed 2 years ago

49b7f94a

feat(measure_theory/functions/lp_space): bounds on the sum of functions in L^p, p < 1, and applications (#18796)

sgouezel committed 2 years ago

13bf7613

feat(algebra/module/submodule/basic): add has_vadd (#18815)

xroblot committed 2 years ago

155d5519

Older