leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into YK-cont-alternating

urkud committed 2 years ago

2851eeab

feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087)

YaelDillies committed 2 years ago

65a1391a

feat(combinatorics/simple_graph): More clique lemmas (#19203)

YaelDillies committed 2 years ago

3365b20c

feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)

YaelDillies committed 2 years ago

b1abe23a

move old README.md to OLD_README.md

jcommelin committed 2 years ago

19c869ef

doc: Add a warning mentioning Lean 4 to the readme (#19243)

eric-wieser committed 2 years ago

3ac76ec5

feat(topology/metric_space): diameter of pointwise zero and addition (#19028)

eric-wieser committed 2 years ago

c8f30551

feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629)

YaelDillies committed 2 years ago

ce64cd31

feat(probability/independence): Independence of singletons (#18506)

YaelDillies committed 2 years ago

001ffdc4

feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612)

YaelDillies committed 2 years ago

8818fdef

feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989)

YaelDillies committed 2 years ago

442a83d7

chore(order/liminf_limsup): Generalise and move lemmas (#18628)

YaelDillies committed 2 years ago

ffde2d8a

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (#17926)

joelriou committed 2 years ago

32a7e535

feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352)

YaelDillies committed 2 years ago

48a058d7

feat(analysis/convex/proj_Icc): Extending convex functions (#18797)

YaelDillies committed 2 years ago

3ba15165

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)

joelriou committed 2 years ago

63721b2c

feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863)

hrmacbeth committed 2 years ago

3b522651

feat(linear_algebra/orientation): add `orientation.reindex` (#19236)

eric-wieser committed 2 years ago

0c1d80f5

feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (#17828)

bottine committed 2 years ago

188a411e

feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (#15260)

vihdzp committed 2 years ago

8900d545

feat(tactic/positivity): Extension for `ite` (#17650)

YaelDillies committed 2 years ago

e90e0a61

feat(analysis/normed_space/continuous_linear_map): generalize typeclass assumptions (#19108)

eric-wieser committed 2 years ago

fe18deda

feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)

eric-wieser committed 2 years ago

d11f435d

feat(algebraic_topology/dold_kan): tools for compatibilities, lemmas (#17923)

joelriou committed 2 years ago

18ee5998

feat(order/upper_lower/basic): Linear order (#19068)

YaelDillies committed 2 years ago

c0c52abb

fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965)

eric-wieser committed 2 years ago

4be58905

docs(topology/dense_embedding): Improve explanation (#18134)

YaelDillies committed 2 years ago

148aefbd

chore(ring_theory/kaehler): cleanup instances (#19234)

eric-wieser committed 2 years ago

4b92a463

feat(ring_theory/tensor_product): add missing scalar tower instances (#19143)

eric-wieser committed 2 years ago

88fcdc3d

feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875)

eric-wieser committed 2 years ago

8047de4d

Older