# Zulip Chat Archive

## Stream: triage

### Topics:

- PR #13862: feat(ring_theory/ideal/nc_jacobson_radical): J… (2 messages, latest: Jan 31 2023 at 14:09)
- issue #15565: Locally convex Hausdorff spaces (4 messages, latest: Jan 31 2023 at 14:09)
- PR #14694: refactor(topology): drop
`uniformity`

(2 messages, latest: Jan 30 2023 at 14:09) - issue #3273: squeeze_simp also simplify targets (7 messages, latest: Jan 30 2023 at 14:09)
- PR #17142: fix(tactic/polyrith): fix crash when hypothese… (3 messages, latest: Jan 29 2023 at 16:08)
- PR #10255: feat(linear_algebra/tensor_power): the tensor … (7 messages, latest: Jan 29 2023 at 14:46)
- issue #2534: Get rid of
`is_(semi)ring_hom`

(9 messages, latest: Jan 29 2023 at 14:08) - issue #3655:
`interval_cases`

for`pnat`

s does not work, … (5 messages, latest: Jan 28 2023 at 14:09) - PR #17921: feat(category_theory/idempotents): idempotent … (1 message, latest: Jan 27 2023 at 14:09)
- issue #3349: assoc_rw can leave side-goals as metavariables (16 messages, latest: Jan 27 2023 at 14:09)
- PR #9692: refactor(algebra/star): replace
`star_ring_aut`

… (3 messages, latest: Jan 26 2023 at 14:08) - issue #2724: have
`solve_by_elim`

call`intro1`

before gi… (6 messages, latest: Jan 26 2023 at 14:08) - PR #14870: feat(analysis/inner_product_space/spectrum): a… (1 message, latest: Jan 25 2023 at 14:08)
- issue #18135: The Shapley-Folkman lemma (1 message, latest: Jan 25 2023 at 14:08)
- issue #1142: Etale cohomology (10 messages, latest: Jan 24 2023 at 16:14)
- PR #15347: feat(tactic/polyrith): polyrith at h (1 message, latest: Jan 24 2023 at 14:08)
- [PR #17006: feat(category_theory/
*): Monoid objects in Abe…](topic/PR.20.2317006.3A.20feat(category_theory.2F*).3A.20Monoid.20objects.20in.20Abe.2E.2E.2E.html) (1 message, latest: Jan 23 2023 at 14:08) - issue #15723:
`expand_exists`

improvements (3 messages, latest: Jan 23 2023 at 14:08) - PR #13937: WIP(analysis/convolution): Define convolution … (2 messages, latest: Jan 22 2023 at 14:08)
- issue #2016: Formal roadmaps need to be explained and doc… (5 messages, latest: Jan 22 2023 at 14:08)
- PR #17886: chore(data/finset/image): reduce imports (1 message, latest: Jan 21 2023 at 14:08)
- issue #1038: Implement computable real numbers (8 messages, latest: Jan 21 2023 at 14:08)
- [PR #8196: feat(topology/{extremally_disconnected, stone_c…](topic/PR.20.238196.3A.20feat(topology.2F.7Bextremally_disconnected.2C.20stone_c.2E.2E.2E.html) (5 messages, latest: Jan 20 2023 at 14:08)
- issue #2409: Linter
`doc_blame`

generates unwanted warnin… (12 messages, latest: Jan 20 2023 at 14:08) - PR #18066: chore(deprecated): delete deprecated folder (1 message, latest: Jan 19 2023 at 14:09)
- issue #3120: a non-interactive version of
`squeeze_simp`

,… (5 messages, latest: Jan 19 2023 at 14:09) - [PR #17164: feat(analysis/normed_space/star/continuous_fun…](topic/PR.20.2317164.3A.20feat(analysis.2Fnormed_space.2Fstar.2Fcontinuous_fun.2E.2E.2E.html) (1 message, latest: Jan 18 2023 at 14:09)
- issue #2730: computer algebra system style tactics? (7 messages, latest: Jan 18 2023 at 14:09)
- PR #11771: feat(computability/partrec_arity): partial rec… (2 messages, latest: Jan 17 2023 at 14:08)
- issue #5489: @[simps] improvements (3 messages, latest: Jan 17 2023 at 14:08)
- PR #10963: feat(combinatorics/graph): typeclasses for gra… (5 messages, latest: Jan 16 2023 at 14:08)
- issue #5659: suggest and show_term give incorrect suggest… (5 messages, latest: Jan 16 2023 at 14:08)
- issue #4014: Miracle Flatness and Zariski's Main Theorem (30 messages, latest: Jan 15 2023 at 22:11)
- issue #5901: simp? and squeeze_simp (11 messages, latest: Jan 15 2023 at 14:12)
- PR #3515: feat(data/dfinsupp): Add an equivalence between… (7 messages, latest: Jan 15 2023 at 14:08)
- PR #6887: feat(analysis/special_functions/pow): Add Berno… (4 messages, latest: Jan 14 2023 at 14:09)
- PR #13500: uniform_limit_of_holo_is_holo (4 messages, latest: Jan 13 2023 at 14:30)
- issue #10696:
`@\[mk_iff\]`

causes a type error (3 messages, latest: Jan 13 2023 at 14:09) - PR #6045: refactor(algebra/group/type_tags): make additiv… (1 message, latest: Jan 12 2023 at 14:10)
- issue #16932: Diamond of complete boolean algebras on sets (1 message, latest: Jan 12 2023 at 14:10)
- PR #14863: refactor(order/complete_lattice): ditch `compl… (1 message, latest: Jan 11 2023 at 14:09)
- issue #1858: Define Banach algebras (9 messages, latest: Jan 11 2023 at 14:09)
- PR #10632: feat(geometry/euclidean/ceva) : Ceva's Theorem… (5 messages, latest: Jan 10 2023 at 14:08)
- PR #17291: feat(geometry/manifold/cont_mdiff): local stru… (1 message, latest: Jan 09 2023 at 14:09)
- issue #11186: Make
`to_ring_hom_eq_coe`

into a`simp`

lem… (5 messages, latest: Jan 09 2023 at 14:09) - issue #15992: evaluate
`int.floor`

and`int.fract`

with `… (5 messages, latest: Jan 08 2023 at 14:32) - PR #11000: feat(combinatorics/graph/basic): Graph hierarc… (5 messages, latest: Jan 08 2023 at 14:08)
- PR #17302: feat(geometry/manifold/vector_bundle): `smooth… (2 messages, latest: Jan 08 2023 at 13:31)
- issue #11523: Develop basic theory of integrally closed d… (3 messages, latest: Jan 07 2023 at 16:21)
- PR #15910: feat(data/multiset/basic): more basic lemmas o… (1 message, latest: Jan 06 2023 at 14:09)
- issue #1539: Improve dense_embedding documentation (10 messages, latest: Jan 06 2023 at 14:09)
- PR #5891: feat(combinatorics/simple_graph/basic): add edg… (6 messages, latest: Jan 05 2023 at 14:12)
- issue #1496: Merge 3 files about basic properties of rela… (11 messages, latest: Jan 05 2023 at 14:09)
- PR #9828: feat(group_theory): class equation for finite g… (5 messages, latest: Jan 04 2023 at 14:08)
- issue #17919: Q: ChatGPT etc. trained on mathlib and tests (2 messages, latest: Jan 04 2023 at 00:44)
- PR #17483: feat(algebra/group/basic): add some lemmas on … (1 message, latest: Jan 03 2023 at 14:08)
- issue #3095: Document rw configuration (10 messages, latest: Jan 02 2023 at 14:09)
- PR #11364: feat(algebra/char_p/basic): refactor proof of … (1 message, latest: Jan 02 2023 at 14:08)
- [issue #15053: Add an instance `{add_,}sub{monoid,group}
*c…](topic/issue.20.2315053.3A.20Add.20an.20instance.20.60.7Badd*.2C.7Dsub.7Bmonoid.2Cgroup.7D_c.2E.2E.2E.html) (3 messages, latest: Jan 02 2023 at 09:16) - PR #15168: feat(order/antisymm_incomp): move antisymmetri… (1 message, latest: Jan 01 2023 at 14:09)
- PR #13791: refactor(algebra/monoid_algebra): remove simp … (2 messages, latest: Dec 31 2022 at 14:08)
- issue #15566: Define Hermite polynomials (4 messages, latest: Dec 31 2022 at 14:08)
- PR #14228: chore(various files):
`move_add`

-driven acts o… (1 message, latest: Dec 30 2022 at 14:08) - issue #4971: Jordan normal form (7 messages, latest: Dec 30 2022 at 14:08)
- PR #16645: chore(data/real/nnreal): make
`real.to_nnreal`

… (1 message, latest: Dec 29 2022 at 14:08) - issue #2179: Define exact sequences (11 messages, latest: Dec 28 2022 at 14:08)
- PR #17653: feat(ring_theory/integral_domain): generalize … (1 message, latest: Dec 27 2022 at 14:08)
- PR #17939: feat(order/locally_finite):
`finset.interval`

(2 messages, latest: Dec 26 2022 at 14:09) - issue #1867: Rethink and document the
`import`

hierarchy … (6 messages, latest: Dec 26 2022 at 14:09) - PR #15954: feat(analysis/transcendental): e is transcende… (2 messages, latest: Dec 25 2022 at 14:09)
- issue #14994: nth_rewrite incorrectly unifies universe va… (3 messages, latest: Dec 25 2022 at 14:08)
- PR #16998: feat(ring_theory/zmod): add criterion for zmod… (1 message, latest: Dec 24 2022 at 14:08)
- issue #10704:
`partial_order.lift`

vs `function.injective… (2 messages, latest: Dec 24 2022 at 14:08) - PR #17654: feat(combinatorics/simple_graph/connectivity):… (1 message, latest: Dec 23 2022 at 14:09)
- issue #4033: properties of (sub)modules (19 messages, latest: Dec 23 2022 at 14:09)
- PR #17012: feat(data/finsupp/basic): Lemmas regarding `fi… (2 messages, latest: Dec 22 2022 at 14:13)
- issue #3533: document
`derive`

/`derive_handler`

attributes (4 messages, latest: Dec 22 2022 at 14:09) - PR #16983: feat(geometry/manifold/cont_mdiff_mfderiv): mo… (1 message, latest: Dec 21 2022 at 14:09)
- issue #6123:
`ext`

recurses into subgoals,`ext x y z`

an… (9 messages, latest: Dec 21 2022 at 14:09) - PR #17426: feat(topology/order/lower_topology): Introduce… (1 message, latest: Dec 20 2022 at 14:08)
- issue #2367: interval_cases bugs (5 messages, latest: Dec 19 2022 at 22:29)
- PR #12933: feat(analysis/cauchy_equation): Add Cauchy's F… (5 messages, latest: Dec 19 2022 at 14:08)
- PR #17081: feat(analysis/convex/continuous): Convex funct… (4 messages, latest: Dec 19 2022 at 08:28)
- issue #4779: refine_struct: case tags not working? (8 messages, latest: Dec 18 2022 at 14:08)
- PR #15171: chore(topology/algebra/group): generalise inst… (1 message, latest: Dec 17 2022 at 14:08)
- issue #11022: The long line (9 messages, latest: Dec 16 2022 at 14:10)
- PR #17200: feat(tactic/abel): separate out abel_nf (1 message, latest: Dec 16 2022 at 14:08)
- PR #17715: feat(analysis/normed_space/compact_operator): … (1 message, latest: Dec 15 2022 at 14:08)
- issue #4616: Follow-ups from
`free_algebra`

, `exterior_al… (8 messages, latest: Dec 15 2022 at 14:08) - PR #15289: chore(set_theory/game/pgame): golf
`le`

and `l… (1 message, latest: Dec 14 2022 at 14:08) - [✔ PR #11545: WIP feat(
*): define subobject classes up to …](topic/.E2.9C.94.20PR.20.2311545.3A.20WIP.20feat(*).3A.20define.20subobject.20classes.20up.20to.20.2E.2E.2E.html) (3 messages, latest: Dec 13 2022 at 14:32) - issue #15907: Refactor bilinear forms (3 messages, latest: Dec 13 2022 at 14:08)
- PR #6485: Add a linter for incorrectly used decidable arg… (33 messages, latest: Dec 12 2022 at 14:08)
- issue #16386: Basics of tempered distributions (2 messages, latest: Dec 12 2022 at 14:08)
- PR #10645: feat(combinatorics/additive/small_roth): Small… (7 messages, latest: Dec 11 2022 at 17:40)
- PR #17249: feat(analysis/seminorm): characterize continui… (2 messages, latest: Dec 10 2022 at 17:18)
- issue #3088: Towards a more beginner-friendly tactic doc (21 messages, latest: Dec 10 2022 at 14:08)
- issue #11388: Limits and continuity for
`real.logb`

(3 messages, latest: Dec 09 2022 at 14:09) - PR #7498: feat(combinatorics/simple_graph/inc_matrix): Or… (1 message, latest: Dec 08 2022 at 14:08)
- issue #1465: Probably
`setup_tactic_parser`

can be integr… (17 messages, latest: Dec 07 2022 at 22:04) - PR #12992: feat(algebra/parity): Squares and primality (1 message, latest: Dec 07 2022 at 14:09)
- PR #17010: feat(src/ring_theory/is_tensor_product): Base … (1 message, latest: Dec 06 2022 at 14:08)
- PR #11448: feat(algebraic_geometry): Quasi-compact morphisms (2 messages, latest: Dec 05 2022 at 14:08)
- [PR #17643: feat(linear_algebra/affine_space/finite_dimens…](topic/PR.20.2317643.3A.20feat(linear_algebra.2Faffine_space.2Ffinite_dimens.2E.2E.2E.html) (1 message, latest: Dec 04 2022 at 14:08)
- issue #2710: More on quotients of categories (8 messages, latest: Dec 04 2022 at 14:08)
- PR #13412: feat(topology/algebra/affine): define topologi… (1 message, latest: Dec 03 2022 at 14:08)
- PR #15260: feat(set_theory/game/pgame): small sets of pre… (1 message, latest: Dec 01 2022 at 14:08)
- issue #7003: Add a user command to print the declarations… (6 messages, latest: Dec 01 2022 at 14:08)
- PR #10683: feat(geometry/manifold): The preimage straight… (2 messages, latest: Nov 30 2022 at 14:09)
- issue #13506: convert
`is_monoid_hom`

etc to structures, … (3 messages, latest: Nov 30 2022 at 14:09) - PR #17525: feat(geometry/euclidean/angle/oriented/basic):… (1 message, latest: Nov 29 2022 at 14:08)
- PR #17055: feat(group_theory/group_action/support): Suppo… (1 message, latest: Nov 28 2022 at 14:08)
- PR #17590: feat(measure_theory/group/action): `smul_invar… (1 message, latest: Nov 27 2022 at 14:08)
- issue #7626: Create
`has_antidiagonal`

class (5 messages, latest: Nov 27 2022 at 14:08) - PR #16997: feat(algebra/ring/divisibility): add sub versi… (1 message, latest: Nov 26 2022 at 14:09)
- issue #11407: Arithmetic of quadratic fields (4 messages, latest: Nov 26 2022 at 14:09)
- PR #7652: feat(tactic/frozen): add tactics about frozen l… (4 messages, latest: Nov 25 2022 at 14:08)
- issue #3082: Hasse invariant of quadratic forms (7 messages, latest: Nov 25 2022 at 14:08)
- PR #15681: feat(topology/homotopy/homotopy_group): `group… (1 message, latest: Nov 24 2022 at 14:08)
- issue #2102: Document
`_eta`

,`_beta`

etc in`naming`

(7 messages, latest: Nov 24 2022 at 14:08) - PR #10254: feat(tactic/declare): canonical declarations (2 messages, latest: Nov 23 2022 at 14:08)
- PR #15179: feat(order/rel_iso):
`well_founded_lt`

instanc… (1 message, latest: Nov 20 2022 at 14:07) - PR #16760: refactor(algebra/opposites): remove irreducibl… (1 message, latest: Nov 19 2022 at 14:07)
- issue #15734: Banach-Alaoglu for topological vector spaces (3 messages, latest: Nov 19 2022 at 14:07)
- issue #15749: Remove
`has_coe_to_fun`

instance for `unita… (1 message, latest: Nov 18 2022 at 14:07) - PR #15901: feat(data/mv_polynomial/pi): `exists_smodeq_of… (1 message, latest: Nov 17 2022 at 14:08)
- PR #4348: feat(order/omega-cpo): cpos form a cartesian cl… (3 messages, latest: Nov 16 2022 at 14:08)
- PR #16820: feat(algebra/category/Group/injective): Prereq… (1 message, latest: Nov 15 2022 at 14:07)
- [PR #10205: Prove the solutions (and uniqueness of those s…](topic/PR.20.2310205.3A.20Prove.20the.20solutions.20(and.20uniqueness.20of.20those.20s.2E.2E.2E.html) (1 message, latest: Nov 14 2022 at 14:13)
- PR #11807: feat(algebra/category/Module/monoidal): Genera… (1 message, latest: Nov 13 2022 at 14:07)
- [PR #15592: feat(combinatorics/hales_jewett, combinatorics…](topic/PR.20.2315592.3A.20feat(combinatorics.2Fhales_jewett.2C.20combinatorics.2E.2E.2E.html) (1 message, latest: Nov 12 2022 at 14:07)
- PR #6418: feat(algebra/group_with_zero): add lemmas about… (3 messages, latest: Nov 11 2022 at 14:09)
- issue #13574: padic_norm file maintenance (2 messages, latest: Nov 11 2022 at 14:09)
- PR #5719: feat(meta): Assignable datatypes and expression… (4 messages, latest: Nov 10 2022 at 14:16)
- issue #7189: Lemmas produced by
`@\[elementwise\]`

aren't u… (4 messages, latest: Nov 10 2022 at 14:16) - PR #15760: feat(number_theory/prime_counting): Tochiori l… (2 messages, latest: Nov 09 2022 at 14:12)
- issue #2726: a multiplicative version of the
`abel`

tactic (6 messages, latest: Nov 09 2022 at 14:12) - PR #9626: feat(analysis/conformal/inner_product_space): t… (3 messages, latest: Nov 08 2022 at 14:10)
- issue #7691: to_additive-like attribute for order_dual (8 messages, latest: Nov 08 2022 at 14:10)
- PR #8496: refactor(order/conditionally_complete_lattice):… (4 messages, latest: Nov 07 2022 at 14:20)
- [PR #16454: feat(data/finsupp/defs, algebra/big_operators/…](topic/PR.20.2316454.3A.20feat(data.2Ffinsupp.2Fdefs.2C.20algebra.2Fbig_operators.2F.2E.2E.2E.html) (1 message, latest: Nov 06 2022 at 14:17)
- PR #8737: feat(combinatorics/simple_graph): connectivity (1 message, latest: Nov 05 2022 at 14:16)
- PR #11352: feat(data/sum/interval): The lexicographic sum… (2 messages, latest: Nov 04 2022 at 14:17)
- PR #13917: feat(set_theory/game/basic): Golf using `antis… (1 message, latest: Nov 03 2022 at 14:22)
- PR #8475: feat(order/compactly_generated): For any
`b`

, t… (1 message, latest: Nov 02 2022 at 14:26) - issue #1868: Tactic to transfer theorems / definitions us… (4 messages, latest: Nov 02 2022 at 14:26)
- [PR #11985: feat(
*): add additive versions of `is_central_…](topic/PR.20.2311985.3A.20feat(*).3A.20add.20additive.20versions.20of.20.60is_central_.2E.2E.2E.html) (1 message, latest: Nov 01 2022 at 14:26) - PR #6954: feat(archive/imo): add 2014 Q1 (2 messages, latest: Oct 30 2022 at 14:18)
- issue #10954: Add an @[intuit] attribute or similar (7 messages, latest: Oct 29 2022 at 14:41)
- PR #15915: refactor(linear_algebra/smodeq): Relax smodeq … (2 messages, latest: Oct 29 2022 at 14:19)
- PR #15927: feat(order/order_iso_nat): value is accessible… (1 message, latest: Oct 28 2022 at 14:27)
- issue #161: Change list.prod from foldl to foldr (9 messages, latest: Oct 28 2022 at 14:27)
- PR #15547: feat(set_theory/zfc/basic): intersection of fa… (1 message, latest: Oct 27 2022 at 14:29)
- PR #14809: feat(order/has_involution): Types with antiton… (2 messages, latest: Oct 26 2022 at 14:26)
- issue #4688: Unify
`char_zero`

with`char_p`

(3 messages, latest: Oct 26 2022 at 14:26) - PR #16965: feat(data/{finset,set}/basic): A nonempty set … (2 messages, latest: Oct 24 2022 at 15:16)
- [PR #7904: feat(order/basic, algebra/ordered_monoid_lemmas…](topic/PR.20.237904.3A.20feat(order.2Fbasic.2C.20algebra.2Fordered_monoid_lemmas.2E.2E.2E.html) (2 messages, latest: Oct 22 2022 at 18:20)
- issue #15860: Pi is irrational (1 message, latest: Oct 22 2022 at 14:22)
- PR #8979: Modular forms (4 messages, latest: Oct 21 2022 at 19:50)
- issue #14781: Approximation tactic (1 message, latest: Oct 21 2022 at 14:39)
- PR #8516: refactor(data/matrix/basic): Remove matrix.scalar (2 messages, latest: Oct 20 2022 at 14:38)
- issue #2880: integrate
`noncomm_ring`

and`ring`

(2 messages, latest: Oct 20 2022 at 14:38) - PR #11046: Complexity Theory (1 message, latest: Oct 19 2022 at 14:36)
- PR #15990: feat(set_theory/ordinal/arithmetic): miscellan… (1 message, latest: Oct 18 2022 at 14:35)
- PR #14250: feat(computability): prove equivalence of NFAs… (1 message, latest: Oct 17 2022 at 14:39)
- PR #15949: feat(ring_theory/finiteness): A morphism is fi… (5 messages, latest: Oct 16 2022 at 14:43)
- issue #3186: add nice VSCode settings (6 messages, latest: Oct 16 2022 at 14:21)
- PR #16087: feat(topology/covering): Define covering spaces (2 messages, latest: Oct 15 2022 at 15:55)
- PR #11233: feat (group_theory/perm/cycle_type) : add form… (3 messages, latest: Oct 13 2022 at 14:29)
- issue #5518: "simp normal form" should be documented (9 messages, latest: Oct 13 2022 at 14:29)
- PR #5569: feat(algebra/module/submodule): merge smul_mem … (2 messages, latest: Oct 12 2022 at 14:39)
- PR #14350: refactor(linear_algebra/clifford_algebra): rel… (1 message, latest: Oct 11 2022 at 14:34)
- PR #16338: feat(analysis/convex/body): endow with Hausdor… (1 message, latest: Oct 10 2022 at 14:42)
- PR #4059: feat(category_theory/monoidal): Strong functor (2 messages, latest: Oct 09 2022 at 14:21)
- PR #6244: feat(data/fin/tuple): lemmas about append (1 message, latest: Oct 08 2022 at 14:23)
- PR #3770: feat(group/perm/sign): swap_adj_induction_on (8 messages, latest: Oct 07 2022 at 14:36)
- issue #4336:
`ext`

on structures should use `subsingleton… (8 messages, latest: Oct 06 2022 at 14:37) - PR #7707: fix(tactic/induction): fix generalisation with … (5 messages, latest: Oct 05 2022 at 14:46)
- PR #11716: feat(topology/lindelof): define Lindelöf space (3 messages, latest: Oct 04 2022 at 14:39)
- PR #13566: feat(analysis/normed_space/multilinear): parti… (1 message, latest: Oct 03 2022 at 14:38)
- issue #15669: Connected components are open, under suitab… (3 messages, latest: Oct 02 2022 at 14:27)
- PR #8103: feat(geometry/manifold/curves): smooth curves (3 messages, latest: Oct 01 2022 at 14:21)
- issue #2601: Linear programming (12 messages, latest: Oct 01 2022 at 14:21)
- PR #15141: feat(probability/subgaussian): define sub-Gaus… (1 message, latest: Sep 30 2022 at 14:36)
- PR #14855: feat(order/upper_lower, order/hom/basic): Uppe… (1 message, latest: Sep 29 2022 at 14:29)
- issue #10802: Stars and bars (10 messages, latest: Sep 29 2022 at 14:29)
- [PR #11677: feat(order/category/
*): Lattice categories](topic/PR.20.2311677.3A.20feat(order.2Fcategory.2F*).3A.20Lattice.20categories.html) (1 message, latest: Sep 27 2022 at 14:34) - PR #4406: feat(data/tuple): homogeneous tuples based on `… (4 messages, latest: Sep 26 2022 at 14:33)
- issue #2553: Quadratic forms over Q_p (14 messages, latest: Sep 26 2022 at 14:33)
- [PR #15491: feat(combinatorics/set_family/compression/basi…](topic/PR.20.2315491.3A.20feat(combinatorics.2Fset_family.2Fcompression.2Fbasi.2E.2E.2E.html) (2 messages, latest: Sep 25 2022 at 16:06)
- issue #408: transporting definitions and theorems along i… (43 messages, latest: Sep 25 2022 at 14:18)
- PR #16525: chore(algebra/order/monoid_lemmas_zero_lt): re… (1 message, latest: Sep 24 2022 at 14:17)
- issue #3975: remove the coercion from zmod n to other rings (6 messages, latest: Sep 24 2022 at 14:17)
- PR #15047: feat(data/matrix/companion): Companion matrix (1 message, latest: Sep 22 2022 at 14:27)
- PR #15552: feat(set_theory/zfc/ordinal): basic results on… (1 message, latest: Sep 21 2022 at 14:29)
- issue #11571: Lipschitz embeddings into ℓ^∞ (4 messages, latest: Sep 21 2022 at 14:29)
- issue #5504: to_additive should raise an error if the ori… (2 messages, latest: Sep 19 2022 at 14:35)
- PR #10409: feat(data/list/basic): add filter/remove_all l… (2 messages, latest: Sep 19 2022 at 14:25)
- PR #16437: feat(group_theory/commutator): Add `commutator… (2 messages, latest: Sep 18 2022 at 15:26)
- issue #1654: clean up usages of
`ext`

(11 messages, latest: Sep 18 2022 at 14:14) - PR #10119: feat(ring_theory/graded_algebra): `mv_polynomi… (3 messages, latest: Sep 17 2022 at 14:14)
- PR #16267: feat(order/bounded_order): The lattice of comp… (1 message, latest: Sep 16 2022 at 14:25)
- PR #15532: chore(set_theory/ordinal/arithmetic): move the… (1 message, latest: Sep 14 2022 at 14:24)
- PR #4579: feat(tactic/chain_trans): prove inequalities by… (5 messages, latest: Sep 13 2022 at 14:23)
- PR #6259: chore(data/subtype): add heq_of_coe_eq ext lemma (4 messages, latest: Sep 12 2022 at 14:22)
- PR #16276: feat(algebraic_topology/simplex_category): str… (1 message, latest: Sep 11 2022 at 14:14)
- PR #14399: feat(ring_theory/ideal/basic): define right id… (1 message, latest: Sep 10 2022 at 14:14)
- PR #7065: feat(analysis/special_functions/integrals): int… (5 messages, latest: Sep 09 2022 at 14:22)
- issue #12685: let
`linear_combination`

solve`≠`

goals (3 messages, latest: Sep 09 2022 at 14:22) - PR #15849: feat(data/nat/basic): add_base_rec (1 message, latest: Sep 07 2022 at 14:24)
- PR #7436: feat(category_theory/concrete): representably c… (3 messages, latest: Sep 06 2022 at 14:18)
- PR #15041: refactor(set_theory/cardinal/basic): constrain… (1 message, latest: Sep 05 2022 at 14:17)
- PR #16168: feat(data/set/intervals/unordered_interval): I… (2 messages, latest: Sep 04 2022 at 14:28)
- issue #4709: Type vars in
`data/polynomial/splitting_field`

(2 messages, latest: Sep 04 2022 at 14:13) - PR #3638: feat(data/qpf): extend the theory of qpfs to su… (4 messages, latest: Sep 03 2022 at 14:14)
- PR #15996: feat(algebraic_geometry): `exists_pow_mul_eq_… (1 message, latest: Sep 01 2022 at 14:14)
- issue #9945:
`to_additive`

guesses a bad name in some edg… (5 messages, latest: Aug 31 2022 at 14:15) - [PR #9623: feat(analysis/normed_space/conformal_linear_map…](topic/PR.20.239623.3A.20feat(analysis.2Fnormed_space.2Fconformal_linear_map.2E.2E.2E.html) (3 messages, latest: Aug 29 2022 at 14:15)
- PR #12842: feat(algebra/order/floor): Generalize floor le… (2 messages, latest: Aug 28 2022 at 16:21)
- PR #15464: feat(group_theory): Groups of order p^2 are ab… (4 messages, latest: Aug 28 2022 at 08:11)
- PR #15408: feat(set_theory/game/nim): recursors for left/… (1 message, latest: Aug 27 2022 at 14:13)
- PR #16074: feat(number_theory/padics/padic_norm): add int… (1 message, latest: Aug 25 2022 at 14:14)
- issue #16021: Lean is unable to infer
`ordered_smul`

inst… (2 messages, latest: Aug 24 2022 at 14:25) - PR #14769: feat(probability/tail_prob): the tail probabil… (1 message, latest: Aug 24 2022 at 14:13)
- issue #5525: Unify (or at least connect)
`order_hom`

and … (2 messages, latest: Aug 22 2022 at 14:13) - PR #11444: chore(analysis/calculus/fderiv_symmetric): spl… (1 message, latest: Aug 20 2022 at 14:13)
- PR #14659: feat(set_theory/game/pgame): notation and basi… (1 message, latest: Aug 19 2022 at 14:14)
- [PR #11759: refactor(
*): remove duplicate subobject instances](topic/PR.20.2311759.3A.20refactor(*).3A.20remove.20duplicate.20subobject.20instances.html) (1 message, latest: Aug 18 2022 at 14:16) - PR #9843: feat(algebra/group/conj): conjugacy class as fi… (1 message, latest: Aug 17 2022 at 14:19)
- PR #12587: feat(algebra/ring/basic): lemmas about oddness… (2 messages, latest: Aug 16 2022 at 17:55)
- PR #14734: refactor(algebra/module/dedekind_domain): elim… (1 message, latest: Aug 15 2022 at 14:16)
- [PR #15206: chore(
*): golf and tidy some proofs](topic/PR.20.2315206.3A.20chore(*).3A.20golf.20and.20tidy.20some.20proofs.html) (1 message, latest: Aug 14 2022 at 14:13) - PR #11376: feat(ring_theory/dedekind_finite): add materia… (1 message, latest: Aug 13 2022 at 14:13)
- PR #5179: feat(linear_algebra/multilinear-tensor): Add `m… (5 messages, latest: Aug 12 2022 at 14:14)
- PR #14494: feat(computability/timed): add complexity anal… (1 message, latest: Aug 11 2022 at 14:13)
- [PR #15159: feat(number_theory/modular_forms/congruence_su…](topic/PR.20.2315159.3A.20feat(number_theory.2Fmodular_forms.2Fcongruence_su.2E.2E.2E.html) (1 message, latest: Aug 09 2022 at 14:18)
- [PR #14534: feat(topology/uniform_space/uniform_convergenc…](topic/PR.20.2314534.3A.20feat(topology.2Funiform_space.2Funiform_convergenc.2E.2E.2E.html) (2 messages, latest: Aug 08 2022 at 14:42)
- PR #8399: feat(archive): mccune axiom defines groups (4 messages, latest: Aug 07 2022 at 14:13)
- PR #15071: refactor(order/well_founded): ditch `well_foun… (2 messages, latest: Aug 06 2022 at 16:46)
- issue #14902: Composition of convex functions (2 messages, latest: Aug 06 2022 at 14:43)
- PR #10830: feat(algebraic_geometry): descent theorem (1 message, latest: Aug 05 2022 at 14:15)
- PR #13240: feat(data/polynomial/zcoeff): define zcoeff + API (2 messages, latest: Aug 04 2022 at 14:23)
- PR #13675: refactor(topology/metric_space/basic): migrate… (1 message, latest: Aug 03 2022 at 14:13)
- issue #14993: apply' can close the goal with metavariables (1 message, latest: Aug 03 2022 at 14:13)
- PR #15644: feat(algebra/order/with_zero): Add eq_one_of_m… (1 message, latest: Aug 02 2022 at 14:14)
- PR #14382: feat(analysis/analytic/isolated_zeros): princi… (1 message, latest: Aug 01 2022 at 14:16)
- PR #15233: refactor(set_theory/cardinal/basic): `enat.car… (2 messages, latest: Jul 31 2022 at 17:56)
- issue #1046: Expand the surreals library (7 messages, latest: Jul 30 2022 at 21:22)
- PR #14812: refactor(algebra/direct_sum/module): use `deco… (1 message, latest: Jul 30 2022 at 14:13)
- PR #12312: feat(analysis/inner_product_space/sqrt): `is_s… (2 messages, latest: Jul 29 2022 at 14:13)
- PR #15550: feat(set_theory/zfc/basic):
`pSet`

with empty … (4 messages, latest: Jul 29 2022 at 06:56) - PR #14335: feat(data/sign): Allocating signs (1 message, latest: Jul 27 2022 at 14:15)
- PR #10643: feat(data/set_like/basic): add a congr lemma (1 message, latest: Jul 25 2022 at 14:15)
- PR #11468: feat(linear_algebra/clifford_algebra): the cli… (1 message, latest: Jul 24 2022 at 14:12)
- issue #1509: wlog (6 messages, latest: Jul 23 2022 at 14:13)
- PR #14807: feat(order/interval): Order intervals (1 message, latest: Jul 21 2022 at 14:14)
- PR #9056: feat(group_theory/nilpotent): add lemma on quot… (4 messages, latest: Jul 20 2022 at 14:15)
- issue #199: TODO: unify
`disjoint`

(7 messages, latest: Jul 20 2022 at 11:27) - PR #11553: feat(algebra/jordan/triple): Introduce Jordan … (2 messages, latest: Jul 19 2022 at 14:14)
- PR #12900: feat(order/hom/lattice): Map lattice homs alon… (1 message, latest: Jul 18 2022 at 14:22)
- [PR #13200: feat(ring_theory/polynomial/special_coefficien…](topic/PR.20.2313200.3A.20feat(ring_theory.2Fpolynomial.2Fspecial_coefficien.2E.2E.2E.html) (1 message, latest: Jul 17 2022 at 14:13)
- PR #10346: feat(data/fin/tuple): rename
`fin.append`

to `… (2 messages, latest: Jul 16 2022 at 14:13) - PR #11932: feat(order/sup_indep): More lemmas (2 messages, latest: Jul 14 2022 at 14:18)
- PR #7803: feat(topology): continuous sections of a vector… (2 messages, latest: Jul 13 2022 at 14:16)
- issue #8590: Test that the input
`.bib`

file is exactly t… (4 messages, latest: Jul 13 2022 at 14:16) - PR #14923: fix(algebra/group/units): splitting out `mul_o… (1 message, latest: Jul 12 2022 at 14:23)
- issue #13461:
`to_`

framework (2 messages, latest: Jul 01 2022 at 14:21) - issue #14275: Create library note explaining seemingly re… (1 message, latest: Jun 30 2022 at 14:19)
- PR #12497: refactor(analysis/inner_product_space/pi_L2): … (2 messages, latest: Jun 29 2022 at 14:18)
- PR #13726: definition of triangle_free_far in terms of ed… (2 messages, latest: Jun 28 2022 at 14:19)
- issue #11682: command to unpack an existential with `clas… (2 messages, latest: Jun 28 2022 at 14:19)
- PR #9121: feat(algebra/big_operators/finprod): assorted l… (1 message, latest: Jun 27 2022 at 14:22)
- issue #2109:
`nonneg_of_mul_nonpos_right`

and `nonneg_of_… (8 messages, latest: Jun 26 2022 at 23:56) - PR #10562: feat(data/bool): bnot_ne (3 messages, latest: Jun 26 2022 at 14:18)
- PR #12812: feat(ring_theory/integrally_closed): if x is i… (2 messages, latest: Jun 24 2022 at 14:18)
- PR #6799: chore(analysis/normed_space/inner_product): euc… (3 messages, latest: Jun 23 2022 at 14:19)
- PR #14072: feat(set_theory/ordinal/notation): fast growin… (5 messages, latest: Jun 22 2022 at 18:56)
- PR #10865: feat(order/atoms): A set/finset/multiset is an… (1 message, latest: Jun 20 2022 at 14:19)
- [PR #7020: feat(geometry/manifold/
*): transferring geometr…](topic/PR.20.237020.3A.20feat(geometry.2Fmanifold.2F*).3A.20transferring.20geometr.2E.2E.2E.html) (5 messages, latest: Jun 12 2022 at 14:18) - issue #1063: homological algebra (10 messages, latest: Jun 12 2022 at 14:18)
- PR #12254: feat(number_theory/miller_rabin): adding lemma… (2 messages, latest: Jun 11 2022 at 14:18)
- issue #1462: Why are sheaves, sheaves? (5 messages, latest: Jun 11 2022 at 14:18)
- PR #11656: feat(algebra/incidence): Incidence algebras (3 messages, latest: Jun 08 2022 at 18:03)
- issue #4985: Avoid restating multiplicatively many `foo_h… (8 messages, latest: Jun 07 2022 at 14:20)
- PR #14044: feat(algebraic_topology/dold_kan): technical l… (1 message, latest: Jun 06 2022 at 14:18)
- PR #10345: feat(linear_algebra/tensor_product): Generalis… (1 message, latest: Jun 05 2022 at 14:18)
- PR #1083: feat(tactic/vampire): interface with Vampire (7 messages, latest: Jun 03 2022 at 14:18)
- PR #5924: chore(data/dfinsupp): Add sum_hom (5 messages, latest: Jun 02 2022 at 14:24)
- PR #12301: refactor(data/nat/factorization): Change defin… (2 messages, latest: May 30 2022 at 14:21)
- PR #3748: WIP: new datatype compiler (5 messages, latest: May 29 2022 at 14:20)
- [PR #12349: feat(
*): fun_like instances on subtypes](topic/PR.20.2312349.3A.20feat(*).3A.20fun_like.20instances.20on.20subtypes.html) (1 message, latest: May 28 2022 at 14:20) - PR #11609: feat(bors.toml): let bors wait for PRs to be g… (2 messages, latest: May 26 2022 at 14:21)
- PR #14030: feat(category_theory/limits): the image of a c… (1 message, latest: May 25 2022 at 14:32)
- issue #10248: fin_cases for finsets not as versatile as m… (3 messages, latest: May 24 2022 at 14:21)
- PR #4739: feat(group_theory/perm/sign): Add `equiv.perm.m… (2 messages, latest: May 22 2022 at 14:20)
- issue #4906: Redefine
`linear_map.tensor`

to be a bundled… (4 messages, latest: May 22 2022 at 14:20) - [PR #8919: refactor(field_theory/
*): generalize subfields …](topic/PR.20.238919.3A.20refactor(field_theory.2F*).3A.20generalize.20subfields.20.2E.2E.2E.html) (2 messages, latest: May 21 2022 at 15:16) - PR #12253: refactor(analysis/inner_product_space/pi_L2): … (1 message, latest: May 20 2022 at 14:20)
- issue #1117: RFC: turn
`mul_action`

into a`structure`

(12 messages, latest: May 20 2022 at 14:20) - PR #4798: feat(analysis/normed_space/dual): dual inner pr… (8 messages, latest: May 19 2022 at 14:20)
- issue #1260: documenting mathlib (14 messages, latest: May 19 2022 at 00:43)
- PR #12964: feat(topology/bornology/order): complete latti… (1 message, latest: May 18 2022 at 14:24)
- PR #2819: feat(number_theory/geometry_of_numbers): Minkow… (2 messages, latest: May 17 2022 at 14:32)
- PR #13480: feat(analysis/convex/uniform): Uniformly conve… (2 messages, latest: May 16 2022 at 14:33)
- issue #1097: transport a monoidal structure across an equ… (3 messages, latest: May 15 2022 at 23:18)
- PR #8632: feat(group_theory/p_group): Groups of order p^2… (11 messages, latest: May 15 2022 at 16:07)
- PR #8054: chore(linear_algebra): make linear_map extend d… (3 messages, latest: May 13 2022 at 16:08)
- issue #2910: Port convexity to affine spaces (4 messages, latest: May 13 2022 at 16:06)
- issue #3532: tfae with named statements (4 messages, latest: May 12 2022 at 14:22)
- PR #4716: chore(category_theory/limits/preserves): preser… (15 messages, latest: May 09 2022 at 14:20)
- issue #2273: Infix notation for
`is_O`

/`is_o`

(3 messages, latest: May 08 2022 at 14:20) - issue #1924: New linters (8 messages, latest: May 06 2022 at 15:56)
- PR #11303: refactor(order/well_founded_set): golf, review… (3 messages, latest: May 06 2022 at 12:22)
- PR #11782: feat(algebra/order/monoid_lemmas_pos): use `co… (4 messages, latest: May 05 2022 at 17:10)
- issue #12666: Integrability on intervals via exhausting t… (1 message, latest: May 03 2022 at 14:18)
- [PR #12009: feat(data/{polynomial, mv_polynomial}/schwartz…](topic/PR.20.2312009.3A.20feat(data.2F.7Bpolynomial.2C.20mv_polynomial.7D.2Fschwartz.2E.2E.2E.html) (1 message, latest: May 02 2022 at 14:20)
- issue #2725:
`push_hom`

and`pull_hom`

tactics (12 messages, latest: May 02 2022 at 14:20) - PR #12118: feat(topology/algebra/module/locally_convex): … (1 message, latest: Apr 30 2022 at 14:19)
- PR #11073: feat(algebra/jordan): Introduce Jordan rings (1 message, latest: Apr 29 2022 at 14:20)
- issue #5059: Geometric Algebra (11 messages, latest: Apr 27 2022 at 09:03)
- PR #7891: feat(algebra/ordered_{field, group}): lemmas ab… (10 messages, latest: Apr 26 2022 at 13:13)
- PR #12310: feat(group_theory/torsion): Q/Z and Fq[X] are … (3 messages, latest: Apr 23 2022 at 15:28)
- issue #4973: Jordan-Chevalley decomposition (5 messages, latest: Apr 22 2022 at 14:20)
- PR #13067: feat(ring_theory/dedekind_domain): Chinese rem… (1 message, latest: Apr 21 2022 at 14:20)
- [PR #11545: WIP feat(
*): define subobject classes up to `s…](topic/PR.20.2311545.3A.20WIP.20feat(*).3A.20define.20subobject.20classes.20up.20to.20.60s.2E.2E.2E.html) (1 message, latest: Apr 18 2022 at 14:13) - PR #12895: feat(algebra/module): add injective module and… (1 message, latest: Apr 15 2022 at 14:14)
- PR #11606: feat(tactic/lint): adding a new linter for iff's (13 messages, latest: Apr 12 2022 at 12:12)
- [PR #8837: feat(algebra/add_torsor, linear_algebra/affine_…](topic/PR.20.238837.3A.20feat(algebra.2Fadd_torsor.2C.20linear_algebra.2Faffine_.2E.2E.2E.html) (3 messages, latest: Apr 10 2022 at 14:13)
- PR #10348: Add whilecc.lean (6 messages, latest: Apr 07 2022 at 14:13)
- PR #10131: feat(list/prod_monoid): add list.prod_map* lemmas (2 messages, latest: Apr 06 2022 at 14:13)
- PR #12478: feat(algebra/algebra/basic): Introduce non-uni… (1 message, latest: Apr 04 2022 at 14:14)
- PR #8781: feat(linear_algebra/{tensor,exterior,clifford})… (1 message, latest: Apr 03 2022 at 14:12)
- PR #11649: feat(algebraic_geometry): Intersection of affi… (1 message, latest: Apr 02 2022 at 14:13)
- [PR #5923: feat(group_theory/perm/sign): Add lemma about (…](topic/PR.20.235923.3A.20feat(group_theory.2Fperm.2Fsign).3A.20Add.20lemma.20about.20(.2E.2E.2E.html) (6 messages, latest: Mar 31 2022 at 14:13)
- PR #3292: feat(field_theory/complete_ordered): conditiona… (2 messages, latest: Mar 30 2022 at 14:28)
- PR #9573: refactor(topology/order): redefine `topological… (3 messages, latest: Mar 29 2022 at 14:13)
- PR #10539: refactor(order): uninstance pi.has_le (2 messages, latest: Mar 27 2022 at 14:17)
- [PR #12186: feat(algebraic_geometry/
*) : presheaf of modules](topic/PR.20.2312186.3A.20feat(algebraic_geometry.2F*).20.3A.20presheaf.20of.20modules.html) (1 message, latest: Mar 25 2022 at 14:13) - PR #9387: feat(probability_theory/independence): if a fam… (1 message, latest: Mar 24 2022 at 14:13)
- PR #8559: feat(analysis/complex/isometry): Homomorphism f… (1 message, latest: Mar 22 2022 at 14:13)
- PR #6476: feat(algebra/ring/boolean_ring): boolean_algebr… (5 messages, latest: Mar 20 2022 at 14:20)
- PR #5527: feat(order/heyting_algebra): Heyting algebras (3 messages, latest: Mar 19 2022 at 14:21)
- issue #2268: caching olean files on a per file basis (3 messages, latest: Mar 19 2022 at 14:13)
- issue #6025: Convert subsingleton lemmas to instances (1 message, latest: Mar 15 2022 at 14:14)
- [PR #11282: feat(
*):*).3A.20.60has_repr.60.20instances.20for.20.60option.60-lik.2E.2E.2E.html) (3 messages, latest: Mar 14 2022 at 16:40)`has_repr`

instances for`option`

-lik…](topic/PR.20.2311282.3A.20feat( - PR #9123: feat(algebra/smul_with_zero): `distrib_mul_acti… (3 messages, latest: Mar 14 2022 at 14:15)
- PR #4956: feat(archive/imo): formalise 1979 Q1 (5 messages, latest: Mar 13 2022 at 15:18)
- [PR #9943: feat(measure_theory/measure/finite_measure_weak…](topic/PR.20.239943.3A.20feat(measure_theory.2Fmeasure.2Ffinite_measure_weak.2E.2E.2E.html) (1 message, latest: Mar 11 2022 at 14:13)
- PR #12046: feat(topology/bornology/hom): Bounded maps (1 message, latest: Mar 10 2022 at 14:12)
- PR #11458: feat(analysis/convex/topology): Separating by … (1 message, latest: Mar 09 2022 at 14:12)
- issue #1068: category instances for all the 'standard' al… (2 messages, latest: Mar 07 2022 at 21:37)
- PR #9525: fix(algebra/ring): fix diamonds in nat- and int… (1 message, latest: Mar 03 2022 at 14:13)
- PR #3332: feat(data/qpf/indexed): indexed families of dat… (7 messages, latest: Mar 03 2022 at 00:58)
- PR #8280: feat(group_theory/quotient_group): the Zassenha… (3 messages, latest: Feb 27 2022 at 14:12)
- issue #4013: properties of ring homomorphisms (16 messages, latest: Feb 26 2022 at 14:13)
- PR #11642: doc(algebra,data/fun_like): small morphism doc… (2 messages, latest: Feb 24 2022 at 14:47)
- PR #11229: feat(topology/continuous_function/compact): co… (1 message, latest: Feb 22 2022 at 14:12)
- PR #10235: refactor(algebra/opposites): use `mul_opposite… (1 message, latest: Feb 20 2022 at 14:12)
- PR #6152: feat(linear_algebra/multilinear): add notation (2 messages, latest: Feb 19 2022 at 14:12)
- issue #1484: unexpected failures with
`omega`

(8 messages, latest: Feb 19 2022 at 14:12) - PR #5574: feat(archive/100-theorems-list): Ballot Problem (14 messages, latest: Feb 16 2022 at 16:27)
- PR #9925: feat(data/nat/choose): add facts about the mult… (1 message, latest: Feb 13 2022 at 14:16)
- PR #11231: feat(measure_theory/function/lp_space): genera… (2 messages, latest: Feb 12 2022 at 14:20)
- issue #2871: unique factorisation of polynomials over a UFD (22 messages, latest: Feb 11 2022 at 18:27)
- PR #10641: refactor(algebra/direct_sum): unbundle `direct… (1 message, latest: Feb 11 2022 at 14:16)
- PRs #6606, #6427, #6428, #6429, #6421 (5 messages, latest: Feb 10 2022 at 05:34)
- PR #10693: feat(data/equiv/basic): lemmas about compositi… (1 message, latest: Feb 09 2022 at 14:16)
- PR #11109: split(data/finsupp/multiset): Split off `data…. (1 message, latest: Feb 08 2022 at 14:17)
- PR #6642: refactor(module/submodule): allow submodules to… (5 messages, latest: Feb 07 2022 at 14:17)
- [PR #8889: feat(algebra/ordered_monoid): sub_neg_monoid (w…](topic/PR.20.238889.3A.20feat(algebra.2Fordered_monoid).3A.20sub_neg_monoid.20(w.2E.2E.2E.html) (1 message, latest: Feb 05 2022 at 14:14)
- issue #2882: apply_congr with h (9 messages, latest: Feb 05 2022 at 01:35)
- PR #10867: feat(combinatorics/simple_graph/inc_matrix): I… (1 message, latest: Feb 02 2022 at 14:16)
- issue #7051: Predicate for Kan extensions (8 messages, latest: Feb 02 2022 at 14:16)
- issue #10728: Alternative dot notation (1 message, latest: Feb 01 2022 at 14:16)
- PR #4259: feat(archive/100-theorems-list): Partition theorem (3 messages, latest: Jan 30 2022 at 14:15)
- issue #2891: support multiple targets in
`equiv_rw`

(8 messages, latest: Jan 29 2022 at 21:22) - PR #10716: feat(algebra/algebra/basic): Algebras are bimo… (1 message, latest: Jan 29 2022 at 14:15)
- PR #11347: refactor(data/equiv/basic): Deduce variants of… (1 message, latest: Jan 28 2022 at 14:16)
- PR #6514: chore(group_theory/submonoid/operations): use c… (1 message, latest: Jan 27 2022 at 14:17)
- issue #7564: Define the Gamma function (1 message, latest: Jan 26 2022 at 14:16)
- PR #8295: feat(geometry/manifold/tangent_bundle): the `ta… (2 messages, latest: Jan 25 2022 at 14:16)
- PR #8289: feat(data/matrix/basic): miscellaneous defs and… (3 messages, latest: Jan 24 2022 at 14:17)
- issue #3097:
`squeeze_simp`

produces invalid result (19 messages, latest: Jan 24 2022 at 14:17) - PR #2508: feat(topology/local_homeomorph): define `local_… (3 messages, latest: Jan 23 2022 at 14:16)
- PR #10140: chore(linear_algebra/multilinear): remove the … (2 messages, latest: Jan 21 2022 at 14:17)
- PR #11095: feat(combinatorics/simple_graph/connectivity):… (1 message, latest: Jan 19 2022 at 14:16)
- PR #9370: feat(field_theory/is_alg_closed/classification)… (2 messages, latest: Jan 15 2022 at 14:17)
- PR #7833: feat(measure_theory/arithmetic): add instances … (1 message, latest: Jan 14 2022 at 14:18)
- issue #5863: Make linters emit messages in a way that's u… (3 messages, latest: Jan 10 2022 at 17:21)
- PR #7980: feat(order/directed): Add codirected_order clas… (2 messages, latest: Jan 08 2022 at 15:41)
- issue #3428: library_search and negation (9 messages, latest: Jan 08 2022 at 14:16)
- PR #4678: feat(tactic/congr): use reducible transparency (3 messages, latest: Jan 07 2022 at 14:17)
- issue #694: We don't have Cauchy's integral formula (12 messages, latest: Jan 06 2022 at 14:49)
- PR #9145: feat(data/mv_polynomial/derivation): derivation… (1 message, latest: Jan 05 2022 at 14:15)
- PR #5521: feat(analysis/calculus/deriv): let simp compute… (7 messages, latest: Jan 03 2022 at 14:17)
- PR #2578: feat(group_theory/free_monoid_product): define … (1 message, latest: Dec 31 2021 at 14:17)
- issue #1093: basic theory of Lie algebras (6 messages, latest: Dec 28 2021 at 12:58)
- issue #10213: Lax-Milgram theorem (1 message, latest: Dec 25 2021 at 14:17)
- PR #10372: feat(linear_algebra/trace): dual_tensor_hom i… (1 message, latest: Dec 22 2021 at 14:18)
- PR #9733: feat(data/set/basic): decidable_mem (2 messages, latest: Dec 21 2021 at 14:17)
- issue #1847: Write a tactic to copy a structure while upd… (2 messages, latest: Dec 21 2021 at 14:17)
- issue #2376: omega is slow with nonstandard 7 (29 messages, latest: Dec 19 2021 at 16:00)
- PR #9490: feat(group_theory/double_cosets): definition of… (1 message, latest: Dec 19 2021 at 14:17)
- issue #687: Linting tools (6 messages, latest: Dec 18 2021 at 14:51)
- PR #10221: doc(algebra/algebra/basic): expand the docstring (5 messages, latest: Dec 15 2021 at 20:16)
- PR #6448: feat(tactic/set): added set_taut to prove set e… (2 messages, latest: Dec 11 2021 at 14:18)
- PR #1822: [WIP] feat(ring_theory/dedekind_finite) some ba… (4 messages, latest: Dec 06 2021 at 14:48)
- PR #7498: feat(combinatorics/simple_graph/inc_matrix): ad… (1 message, latest: Dec 04 2021 at 14:19)
- PR #9545: feat(group_theory/commensurable): Definition an… (1 message, latest: Dec 03 2021 at 14:20)
- PR #8903: feat(analysis): Cauchy integral formula (WIP) (1 message, latest: Dec 02 2021 at 14:19)
- PR #10439: Define compact convergence topology on contino… (2 messages, latest: Dec 01 2021 at 16:40)
- issue #2890:
`equiv_rw`

fails with metavariables (1 message, latest: Dec 01 2021 at 14:20) - PR #10151: chore(data/equiv/transfer_instance): avoid `le… (1 message, latest: Nov 26 2021 at 14:19)
- issue #1098: examples of (symmetric) monoidal categories (4 messages, latest: Nov 25 2021 at 18:06)
- PR #4787: refactor(analysis/convex): redefine
`convex`

fo… (5 messages, latest: Nov 25 2021 at 14:19) - PR #4273: feat(data/set/intervals/with_bot_top): lemmas a… (34 messages, latest: Nov 24 2021 at 14:19)
- PR #8242: feat(category_theory/adjunctions): adjust simp set (2 messages, latest: Nov 22 2021 at 14:19)
- PR #6441: fix(data/list/defs): remove chunking hack (2 messages, latest: Nov 19 2021 at 14:19)
- PR #7274: feat(archive/100-theorems-list): add proof of t… (5 messages, latest: Nov 17 2021 at 14:19)
- PR #2770: feat(combinatorics): Kruskal-Katona theorem and… (2 messages, latest: Nov 11 2021 at 14:19)
- issue #1866: Move
`module`

below`group_power`

in the `im… (5 messages, latest: Nov 10 2021 at 14:20) - issue #1639:
`to_additive`

should copy`simps`

and `exten… (13 messages, latest: Nov 08 2021 at 18:01) - PR #9606: feat(ring_theory/euclidean_domain): generalize … (3 messages, latest: Nov 08 2021 at 11:44)
- PR #8915: feat(number_theory/basic): lifting the exponent… (1 message, latest: Nov 06 2021 at 14:18)
- [PR #8901: refactor(field_theory/
*): generalize subfields …](topic/PR.20.238901.3A.20refactor(field_theory.2F*).3A.20generalize.20subfields.20.2E.2E.2E.html) (1 message, latest: Nov 05 2021 at 14:19) - PR #6295: feat(topology/homeomorph): Add homeomorph_of_co… (2 messages, latest: Nov 02 2021 at 14:19)
- [PR #7645: refactor(algebra/linear_ordered_comm_group_with…](topic/PR.20.237645.3A.20refactor(algebra.2Flinear_ordered_comm_group_with.2E.2E.2E.html) (2 messages, latest: Oct 31 2021 at 14:18)
- PR #2492: refactor(data/polynomial): use `monoid_algebra…. (3 messages, latest: Oct 30 2021 at 14:18)
- issue #946: data.nat.cast.cast is too general to be an in… (17 messages, latest: Oct 30 2021 at 14:18)
- PR #8082: feat(order/succ_pred): define the typeclass `su… (1 message, latest: Oct 29 2021 at 14:19)
- issue #1044: bundling morphisms (16 messages, latest: Oct 28 2021 at 14:39)
- PR #6955: feat(computability/tm_to_partrec): prove finite… (2 messages, latest: Oct 28 2021 at 14:23)
- PR #7093: feat(order/sublattice): sublattice definition (1 message, latest: Oct 27 2021 at 14:19)
- issue #9805: convert proves 1=0 (1 message, latest: Oct 27 2021 at 14:19)
- PR #8981: add file containing the Weierstrass M-test (1 message, latest: Oct 25 2021 at 14:19)
- PR #8154: feat(topology/vector_bundle): `topological_vect… (1 message, latest: Oct 23 2021 at 14:18)
- PR #2784: feat(number_theory/bertrand): Bertrand's postulate (4 messages, latest: Oct 19 2021 at 14:19)
- PR #7539: feat (order/modular_lattice): modular_lattice a… (1 message, latest: Oct 15 2021 at 14:18)
- PR #7206: chore(data/mv_polynomial/basic): make monomial … (1 message, latest: Oct 14 2021 at 14:19)
- issue #4413: document op_induction (2 messages, latest: Oct 11 2021 at 01:20)
- issue #9421: Use
`has_star.star`

instead of`complex.conj`

(2 messages, latest: Oct 09 2021 at 23:23) - PR #7138: feat(combinatorics/simple_graph/basic): add lem… (1 message, latest: Oct 08 2021 at 14:18)
- PR #8913: feat(ring_theory/mv_polynomial/homogeneous): Mu… (1 message, latest: Oct 06 2021 at 14:18)
- PR #6307: feat(algebra/big_operators/order): some variants (2 messages, latest: Oct 05 2021 at 15:03)
- PR #7813: feat(data/nat/digits): Add lemmas (1 message, latest: Oct 04 2021 at 14:18)
- workflow failure (8 messages, latest: May 20 2021 at 06:11)
- [PR #6606: feat(linear_algebra/bilinear_form, linear_algeb…](topic/PR.20.236606.3A.20feat(linear_algebra.2Fbilinear_form.2C.20linear_algeb.2E.2E.2E.html) (1 message, latest: Apr 27 2021 at 14:25)
- issue #2551: Quadratic forms over R — Sylvester's law of … (8 messages, latest: Apr 24 2021 at 14:24)
- [PR #5823: chore(
*) clean up file imports by removing tran…](topic/PR.20.235823.3A.20chore(*).20clean.20up.20file.20imports.20by.20removing.20tran.2E.2E.2E.html) (10 messages, latest: Apr 22 2021 at 14:24) - issue #5258: Abel-Ruffini theorem (3 messages, latest: Apr 21 2021 at 15:20)
- PR #4913: feat(analysis/normed_space/box_subadditive): de… (1 message, latest: Apr 21 2021 at 14:27)
- PR #6244: feat(data/fin): lemmas about append (1 message, latest: Apr 20 2021 at 14:24)
- PR #5927: feat(category_theory/sites): Sheaves of structures (1 message, latest: Apr 17 2021 at 14:22)
- [PR #6741: feat(
*): Add is_scalar_tower instances for tens…](topic/PR.20.236741.3A.20feat(*).3A.20Add.20is_scalar_tower.20instances.20for.20tens.2E.2E.2E.html) (2 messages, latest: Apr 16 2021 at 14:24) - PR #6923: feat(analysis/complex/isometry): add linear_iso… (1 message, latest: Apr 15 2021 at 14:23)
- issue #2176: Define preadditive categories (16 messages, latest: Apr 12 2021 at 03:01)
- PR #3083: refactor(data/finset): use
`lattice`

operations (4 messages, latest: Apr 10 2021 at 14:22) - PR #5539: feat(algebra/field): define division semirings … (2 messages, latest: Apr 08 2021 at 14:24)
- issue #3837:
`@\[simps\]`

does not consider projections of … (4 messages, latest: Apr 08 2021 at 14:24) - [PR #6773: chore(
*): redefine {nat,int} mul based on a lef…](topic/PR.20.236773.3A.20chore(*).3A.20redefine.20.7Bnat.2Cint.7D.20mul.20based.20on.20a.20lef.2E.2E.2E.html) (10 messages, latest: Apr 07 2021 at 21:24) - issue #1608: catch leftover
`set_option`

commands (1 message, latest: Apr 07 2021 at 14:25) - issue #1850: Fundamental theorem of calculus (2 messages, latest: Apr 03 2021 at 14:22)
- PR #6258: feat(ring_theory/laurent_series): introduce rin… (1 message, latest: Apr 02 2021 at 14:23)
- PR #5783: feat(multiset/basic): add lemma exists_minimal_… (2 messages, latest: Mar 28 2021 at 14:23)
- PR #4321: feat(algebra/free_algebra): Define a grading (26 messages, latest: Mar 23 2021 at 08:38)
- PR #6061: feat(tactic/lint): linter for @[class] def (4 messages, latest: Mar 23 2021 at 01:26)
- [PR #5851: chore(
*/pi): rename *_hom.apply to pi.apply_**hom](topic/PR.20.235851.3A.20chore(*.2Fpi).3A.20rename.20*_hom.2Eapply.20to.20pi.2Eapply**_hom.html) (2 messages, latest: Mar 18 2021 at 14:28) - PR #4301: feat(liouville_theorem): lemmas of Liouville th… (14 messages, latest: Mar 17 2021 at 08:17)
- issue #1922: Intuitionistic versions of
`finish`

use clas… (15 messages, latest: Mar 15 2021 at 14:28) - PR #6291: feat(topology/category/profinite): Initial work… (1 message, latest: Mar 14 2021 at 14:21)
- issue #4763: topology/sheaves/sheaf_condition/pairwise_in… (4 messages, latest: Mar 14 2021 at 14:21)
- PR #2292: refactor(algebra/group): make
`multiplicative`

… (53 messages, latest: Mar 13 2021 at 16:05) - PR #3169: feat(ring_theory/polynomial): homogeneous and s… (2 messages, latest: Mar 13 2021 at 14:21)
- PR #2311: Poincaré recurrence theorem (5 messages, latest: Mar 12 2021 at 14:27)
- PR #4615: feat(tactic/converter): Add an exact tactic, to… (8 messages, latest: Mar 11 2021 at 14:26)
- PR #4885: feat(category_theory/adjunction): general adjoi… (4 messages, latest: Mar 08 2021 at 14:44)
- PR #5975: feat(nat/digits): Natural basis representation … (3 messages, latest: Mar 06 2021 at 14:20)
- PR #5487: feat(tactic/to_additive): Allow to_additive aft… (1 message, latest: Mar 01 2021 at 14:20)
- PR #4707: feat(data/polynomial/reverse.lean): show traili… (5 messages, latest: Feb 28 2021 at 14:40)
- PR #2819: [WIP] feat(number_theory/geometry_of_numbers): … (6 messages, latest: Feb 27 2021 at 14:19)
- PR #5152: feat(category_theory): Global Left Kan extension (1 message, latest: Feb 24 2021 at 14:25)
- PR #5966: feat(combinatorics/simple_graph): degree lemmas (1 message, latest: Feb 22 2021 at 14:19)
- PR #4930: feat(category_theory/closed): Exponential ideals (4 messages, latest: Feb 20 2021 at 14:19)
- PR #2300: feat(tactic): tactic block caching (2 messages, latest: Feb 19 2021 at 14:20)
- PR #4069: added statements for trailing_degree, nat_trail… (2 messages, latest: Feb 15 2021 at 14:35)
- PR #5893: doc(data/finset): rewrite finset doc-strings (1 message, latest: Feb 14 2021 at 14:19)
- PR #5104: feat(order/antichain): introduce antichain (2 messages, latest: Feb 13 2021 at 14:19)
- issue #2706: rename
`squeeze_simp`

to`simp?`

and have it… (4 messages, latest: Feb 12 2021 at 15:51) - [PR #4619: refactor(algebra/
*): Attempt to generalize the …](topic/PR.20.234619.3A.20refactor(algebra.2F*).3A.20Attempt.20to.20generalize.20the.20.2E.2E.2E.html) (3 messages, latest: Feb 12 2021 at 14:20) - PR #5672: feat(algebra/subalgebra): Trivial subalgebra ha… (1 message, latest: Feb 08 2021 at 14:19)
- PR #3635: WIP: Remove the requirement from
`ideal`

that t… (4 messages, latest: Feb 07 2021 at 18:50) - issue #4674: Roots in alg closed fields (3 messages, latest: Feb 06 2021 at 14:19)
- PR #4731: feat(archive/imo): formalize 1987Q1 (1 message, latest: Feb 05 2021 at 14:20)
- issue #1481:
`ext?`

should print a trace message (3 messages, latest: Jan 30 2021 at 14:27) - PR #5829: feat(data/equiv/one_sided): Add bundled one-sid… (2 messages, latest: Jan 29 2021 at 16:22)
- issue #5525: Unify (or at least connect)
`preorder_hom`

a… (1 message, latest: Jan 29 2021 at 14:23) - PR #5591: feat(geometry/manifold/instances): sphere is a … (6 messages, latest: Jan 28 2021 at 17:08)
- PR #3980: feat(group_theory/group_action): add Cayley's t… (1 message, latest: Jan 27 2021 at 14:23)
- PR #4832: chore(topology/sheaves/sheaf_condition): first … (2 messages, latest: Jan 25 2021 at 14:46)
- issue #1563: order of element (8 messages, latest: Jan 23 2021 at 16:23)
- issue #1853: Define Bochner integrals over subsets and me… (2 messages, latest: Jan 22 2021 at 14:56)
- PR #4949: chore(linear_algebra/basis): make more args exp… (1 message, latest: Jan 21 2021 at 14:44)
- issue #1093: definition of Lie algebras (11 messages, latest: Jan 16 2021 at 16:01)
- PR #5462: feat(data/buffer/parser/numeral): numeral parse… (2 messages, latest: Jan 15 2021 at 20:10)
- PR #4756: feat(algebra/category/Module): direct limit is … (3 messages, latest: Jan 13 2021 at 14:45)
- issue #2672: Bug in ring tactic (3 messages, latest: Jan 12 2021 at 16:38)
- PR #2630: refactor(computability/reduce): define many-one… (5 messages, latest: Jan 11 2021 at 15:48)
- issue #3326: non-idempotence of ring (when following zify) (3 messages, latest: Jan 09 2021 at 14:36)
- PR #5010: feat(data/fin): identities in add and mul monoids (2 messages, latest: Jan 08 2021 at 14:50)
- PR #5361: feat(analysis/real/polynomial): preparations fo… (2 messages, latest: Jan 04 2021 at 14:43)
- issue #2889: missing instance
`equiv_functor unique`

(1 message, latest: Dec 30 2020 at 14:29) - PR #4812: feat(algebra/graded_algebra): Define a dependen… (6 messages, latest: Dec 28 2020 at 14:54)
- PR #5282: feat(category_theory/sites): closed sieves (2 messages, latest: Dec 27 2020 at 14:37)
- PR #5269: feat(linear_algebra/alternating): Add dom_coprod (2 messages, latest: Dec 25 2020 at 14:34)
- issue #2872: ideal.is_coprime is about elements not ideal… (4 messages, latest: Dec 18 2020 at 18:30)
- PR #5000: feat(measure_theory/measure_space): add theorem… (1 message, latest: Dec 17 2020 at 14:26)
- PR #4458: feat(analysis/calculus): define a smooth bump f… (3 messages, latest: Dec 15 2020 at 19:05)
- issue #1535: have
`library_search`

call`symmetry`

before… (4 messages, latest: Dec 14 2020 at 15:53) - PR #4773: feat(ring_theory/tensor_product): the base chan… (1 message, latest: Dec 13 2020 at 14:24)
- PR #4658: feat(topology/vector_bundle): definition of top… (4 messages, latest: Dec 10 2020 at 14:24)
- PR #4867: feat(algebra/continued_fractions): add terminat… (1 message, latest: Dec 08 2020 at 14:24)
- PR #2843: refactor(algebra/group/basic): minimal axioms f… (2 messages, latest: Dec 06 2020 at 18:55)
- PR #4843: feat(dynamics): (semi-)flows, omega limits (5 messages, latest: Dec 03 2020 at 14:45)
- PR #4406: feat(data/finvec): homogeneous vectors based on… (2 messages, latest: Dec 02 2020 at 14:24)
- PR #3770: feat(linear_algebra): algebra multilinear maps (11 messages, latest: Dec 01 2020 at 09:22)
- [PR #4817: chore(
*): Test leanprover-community/lean#495](topic/PR.20.234817.3A.20chore(*).3A.20Test.20leanprover-community.2Flean.23495.html) (1 message, latest: Nov 28 2020 at 14:19) - issue #4449: Migrate
`is_Z_bilin`

to the general theory (1 message, latest: Nov 27 2020 at 14:20) - issue #1534: add variations of
`nat.mod_add_div`

(1 message, latest: Nov 24 2020 at 14:20) - issue #4210: to_additive fails for integer literals (1 message, latest: Nov 22 2020 at 14:18)
- PR #4718: feat(tactic/explode): display exploded proofs a… (6 messages, latest: Nov 21 2020 at 06:14)
- PR #4841: feat(tactic/rewrite_search): Automatically sear… (3 messages, latest: Nov 16 2020 at 14:29)
- issue #930: feat(algebra): add additive versions for free… (4 messages, latest: Nov 13 2020 at 18:02)
- PR #4608: feat(category_theory/sites): sheaves on a groth… (7 messages, latest: Nov 13 2020 at 17:36)
- issue #4660: Library note for when implicit arguments are… (3 messages, latest: Nov 11 2020 at 12:16)
- PR #4369: feat(archive/imo): formalize IMO 1964 problem 1 (6 messages, latest: Nov 07 2020 at 21:14)
- random PR: [WIP] feat(number_theory/geometry_of_numbers):… (8 messages, latest: Nov 01 2020 at 22:28)
- random issue: #2726 (7 messages, latest: Nov 01 2020 at 18:44)
- random issue:
`simpa`

accepts non-existing lemmas (#2061) (3 messages, latest: Nov 01 2020 at 16:55) - random issue: transporting definitions and theorems along… (16 messages, latest: Nov 01 2020 at 12:16)
- random PR: #773 (5 messages, latest: Oct 30 2020 at 20:44)
- stream events (4 messages, latest: Oct 30 2020 at 20:34)

Last updated: Jan 31 2023 at 21:29 UTC