Commits leanprover-community/mathlib3

Merge branch 'master' into jordan-triples

mans0954 committed 2 years ago

1914bfa3

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

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

leanprover-community-bot committed 2 years ago

573eea92

chore(set_theory/ordinal/basic): golf (#18547)

astrainfinita committed 2 years ago

8ea5598d

feat(order/irreducible): Sup-irreducible elements (#18999)

YaelDillies committed 2 years ago

bf2428c9

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

leanprover-community-bot committed 2 years ago

08b081ea

fix: handle archive and counterexamples correctly when adding port comments (#19237)

eric-wieser committed 2 years ago

88e6ad41

fix(tactic/linarith): instantiate metavariables in linarith (#19233)

eric-wieser committed 2 years ago

016138c2

feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

vihdzp committed 2 years ago

31b269b6

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

leanprover-community-bot committed 2 years ago

2fe465de

fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981)

eric-wieser committed 2 years ago

c1acdccd

feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738)

eric-wieser committed 2 years ago

6b711d2b

feat(data/*/interval): `finset.uIcc` on concrete structures (#18838)

YaelDillies committed 2 years ago

1d29de43