leanprover-community/mathlib

Pull Requests Commits

Merge branch 'eric-wieser/inv-block' into eric-wieser/inv-block-more

eric-wieser committed 2 years ago

a76edf51

Merge remote-tracking branch 'origin/master' into eric-wieser/inv-block

eric-wieser committed 2 years ago

8619ca6a

refactor(linear_algebra/matrix/nonsingular_inverse): move results about block matrices to `schur_complement` (#18850)

eric-wieser committed 2 years ago

a07a7ae9

chore(zmod/basic): alphabetise imports (#18858)

ericrbg committed 2 years ago

74ad1c88

chore(zmod/basic): remove unneeded import (#18856)

ericrbg committed 2 years ago

473ee9e0

chore(analysis/normed/group/seminorm): use coe_nonneg instead of ℝ≥0.prop (#18833)

kim-em committed 2 years ago

09079525

feat(topology/extremally_disconnected): Extremally disconnected topological spaces (#8196)

adomani committed 2 years ago

7e281def

feat(analysis/calculus/cont_diff): iterated derivatives of maps into clm's (#18756)

mcdoll committed 2 years ago

323b7f26

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

github-actions[bot] committed 2 years ago

4f81bc21

feat(geometry/manifold/vector_bundle/tangent): some equations about trivializations (#18825)

fpvandoorn committed 2 years ago

7dfe8583

feat(measure_theory/integral/integral_eq_improper): fundamental theorem of calculus on (a, +\infty) (#18844)

sgouezel committed 2 years ago

d4817f88

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

YaelDillies committed 2 years ago

52932b3a

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

github-actions[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

eric-wieser committed 2 years ago

fce40afc

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

eric-wieser committed 2 years ago

6fff8770

feat(linear_algebra/matrix/nonsingular_inverse): invertibility of block matrices

eric-wieser committed 2 years ago

84ad3bfb

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

Older