leanprover-community/mathlib3

Pull Requests Commits

fix(analysis/specific_limits/basic)

xgenereux committed 2 years ago

Verified caf9be99

fix(analysis/specific_limits/basic)

xgenereux committed 2 years ago

Verified 80b33d71

fix(analysis/specific_limits/is_R_or_C)

xgenereux committed 2 years ago

Verified f81b141b

feat(analysis/specific_limits/basic)

xgenereux committed 2 years ago

Verified 1d4dbd08

xgenereux committed 2 years ago

Verified fff4a338

feat(analysis /specific_limits/complex)

xgenereux committed 2 years ago

Verified 297872d9

chore(topology/category/Top/limits): split file (#18871)

kim-em committed 2 years ago

178a3265

feat(data/set/pointwise/big_operators): image distributes across pointwise big operators (#18840)

eric-wieser committed 2 years ago

fa2cb8a9

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)

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

Older