leanprover-community/mathlib

Pull Requests Commits

chore(ring_theory/finiteness): generalize `module.finite.trans` (#18880)

eric-wieser committed 2 years ago

fa78268d

feat(linear_algebra/basis): add basis.restrict_scalars (#18814)

xroblot committed 2 years ago

04cdee31

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

leanprover-community-bot committed 2 years ago

9d2f0748

chore(finsupp/basic): weaken hypotheses (#18874)

ericrbg committed 2 years ago

57911c5a

feat(measure_theory/constructions): add the Borel isomorphism theorem. (#18864)

Felix-Weilacher committed 2 years ago

9b2b58d6

chore(algebra/star/basic): generalize quaternion lemmas (#18802)

eric-wieser committed 2 years ago

dc7ac07a

feat(algebra/big_operators/fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817)

YaelDillies committed 2 years ago

cdb01be3

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)

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

Newer Older