Mathlib v3 is deprecated. Go to Mathlib v4

Changelog

2023-10-30 15:07 65a1391a
feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087) …
11 files23 theorems
2023-10-22 19:51 3365b20c
feat(combinatorics/simple_graph): More clique lemmas (#19203) …
7 files63 theorems3 defs
2023-10-16 15:09 b1abe23a
feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976) …
5 files25 theorems
2023-10-11 09:24 19c869ef
move old README.md to OLD_README.md
2 files
2023-10-10 22:55 3ac76ec5
doc: Add a warning mentioning Lean 4 to the readme (#19243) …
1 files
2023-10-09 14:37 c8f30551
feat(topology/metric_space): diameter of pointwise zero and addition (#19028)
5 files9 theorems
2023-09-18 15:31 ce64cd31
feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629) …
2 files13 theorems
2023-09-12 23:46 001ffdc4
feat(probability/independence): Independence of singletons (#18506) …
5 files26 theorems1 defs
2023-09-12 13:12 8818fdef
feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612) …
3 files27 theorems2 defs
2023-08-31 08:51 442a83d7
feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989) …
5 files36 theorems
2023-08-28 11:58 ffde2d8a
chore(order/liminf_limsup): Generalise and move lemmas (#18628) …
5 files29 theorems2 defs
2023-08-05 18:07 32a7e535
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (#17926)
17 files1 theorems4 defs
2023-08-02 16:47 48a058d7
feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352) …
2 files27 theorems1 defs
2023-08-02 13:20 3ba15165
feat(analysis/convex/proj_Icc): Extending convex functions (#18797) …
7 files22 theorems
2023-07-30 10:18 63721b2c
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)
2 files9 theorems5 defs
2023-07-28 12:48 3b522651
feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863) …
5 files16 theorems3 defs
2023-07-28 10:11 0c1d80f5
feat(linear_algebra/orientation): add `orientation.reindex` (#19236)
3 files8 theorems2 defs
2023-07-28 10:11 188a411e
feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (#17828)
1 files19 theorems9 defs
2023-07-28 10:11 8900d545
feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (#15260)
3 files12 theorems2 defs
2023-07-28 07:23 e90e0a61
feat(tactic/positivity): Extension for `ite` (#17650) …
2 files
2023-07-27 10:40 fe18deda
feat(analysis/normed_space/continuous_linear_map): generalize typeclass assumptions (#19108)
1 files
2023-07-26 13:39 d11f435d
feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)
3 files4 theorems6 defs
2023-07-25 05:26 18ee5998
feat(algebraic_topology/dold_kan): tools for compatibilities, lemmas (#17923)
1 files2 theorems5 defs
2023-07-24 11:50 c0c52abb
feat(order/upper_lower/basic): Linear order (#19068) …
3 files2 theorems
2023-07-24 08:57 4be58905
fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965) …
8 files11 theorems1 defs
2023-07-24 08:57 148aefbd
docs(topology/dense_embedding): Improve explanation (#18134) …
1 files
2023-07-24 07:47 4b92a463
chore(ring_theory/kaehler): cleanup instances (#19234) …
2 files1 defs
2023-07-23 09:51 88fcdc3d
feat(ring_theory/tensor_product): add missing scalar tower instances (#19143)
2 files3 theorems
2023-07-22 18:41 8047de4d
feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875) …
1 files8 theorems
2023-07-22 09:12 573eea92
chore(*): add mathlib4 synchronization comments (#19239) …
1 files
2023-07-19 06:33 8ea5598d
chore(set_theory/ordinal/basic): golf (#18547)
2 files2 theorems2 defs
2023-07-16 19:01 bf2428c9
feat(order/irreducible): Sup-irreducible elements (#18999) …
3 files42 theorems4 defs
2023-07-16 12:56 08b081ea
chore(*): add mathlib4 synchronization comments (#19238) …
73 files
2023-07-16 09:47 88e6ad41
fix: handle archive and counterexamples correctly when adding port comments (#19237)
1 files
2023-07-16 09:47 016138c2
fix(tactic/linarith): instantiate metavariables in linarith (#19233) …
6 files
2023-07-16 07:50 31b269b6
feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)
3 files49 theorems2 defs
2023-07-15 12:19 2fe465de
chore(*): add mathlib4 synchronization comments (#19231) …
18 files
2023-07-15 01:08 c1acdccd
fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981) …
3 files
2023-07-15 00:02 6b711d2b
feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738) …
4 files3 theorems1 defs
2023-07-14 19:58 1d29de43
feat(data/*/interval): `finset.uIcc` on concrete structures (#18838) …
13 files60 theorems
2023-07-14 19:58 2c84c2c5
feat(order/well_founded_set): `prod.lex` is well-founded (#18665)
2 files11 theorems
2023-07-14 16:30 d07245fd
feat(group_theory/order_of_element): Order in `α × β` (#18719) …
3 files17 theorems
2023-07-13 13:57 d608fc5d
feat(analysis/calculus/fderiv/mul): derivative of inverse in division rings (#19127)
2 files17 theorems
2023-07-13 10:41 cd391184
feat(*/prod): `prod_prod_prod` equivs (#19235) …
4 files9 theorems4 defs
2023-07-12 21:38 baa88307
feat(analysis/inner_product_space/of_norm): Create an inner product from a norm (#4798) …
3 files10 theorems
2023-07-12 18:27 b01d6eb9
fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument (#19228) …
2 files1 inductives
2023-07-12 18:27 41bef4ae
feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103) …
3 files9 theorems
2023-07-12 15:28 d3b54a9f
fix(tactic/interval_cases): instantiate metavars (#19232) …
2 files
2023-07-12 15:28 d9e96a3e
feat(data/list/dedup): Lemmas about `list.dedup` (#19142) …
2 files6 theorems
2023-07-12 15:28 92bd7b1f
feat(analysis/convex): convexity of n-ary sums (#18943)
4 files10 theorems2 defs