Commits leanprover-community/mathlib

feat(data/matrix/block): injectivity lemmas (#18842)

eric-wieser committed 2 years ago

b5665fd3

feat(measure_theory/measure/haar_of_basis): put the canonical measure on euclidean space (#18870)

eric-wieser committed 2 years ago

83df6d6e

feat(analysis/normed_space/basic): spheres have no interior (#18869)

eric-wieser committed 2 years ago

8000bbbe

chore(set_theory/zfc/basic): reverse `sInter_coe` (#18773)

vihdzp committed 2 years ago

f0b3759a

feat(data/set/finite): Add lemmas relating definitions of infinite sets (#18620)

dignissimus committed 2 years ago

52fa514e

fix(topology/continuous_function/algebra): let `continuous_map.module'` use a `semiring` instead of ` ring` (#18868)

j-loreaux committed 2 years ago

efe03a53

feat(topology/vector_bundle/basic): define in_coordinates (#18826)

fpvandoorn committed 2 years ago

d2d964c6

feat(model_theory/types): Realized types (#17848)

awainverse committed 2 years ago

98bd247d

feat(analysis/calculus/cont_diff): bound for the n-th derivative of a composition (#18643)

sgouezel committed 2 years ago

aa68866e

feat(algebra & polynomial): some (q)smul lemmas+generalisations (#18852)

ericrbg committed 2 years ago

2651125b

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)

leanprover-community-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)

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