Zulip Chat Archive

Stream: mathlib4

---

Topics:

• whnf blowup in Nat.digits (64 messages, latest: Dec 20 2023 at 10:08)
• Problems updating, again (115 messages, latest: Dec 20 2023 at 09:20)
• Rewrite inside IsLittleO (4 messages, latest: Dec 20 2023 at 07:02)
• Squash, Trunc (7 messages, latest: Dec 20 2023 at 02:30)
• continuity and ContinuousOn (14 messages, latest: Dec 20 2023 at 01:06)
• (Mv)Polynomial vs (Mv)PowerSeries (40 messages, latest: Dec 20 2023 at 00:51)
• Tutte's theorem statement (24 messages, latest: Dec 19 2023 at 18:15)
• Inconsistent behaviour of Fin.castPred,Fin.pred, etc. (36 messages, latest: Dec 19 2023 at 10:03)
• example (p : P) : Q := p takes 0.25s to fail! (177 messages, latest: Dec 18 2023 at 22:39)
• TFAE discussion (38 messages, latest: Dec 18 2023 at 22:34)
• ✔ invalid universe level (6 messages, latest: Dec 18 2023 at 19:00)
• ✔ Indexed infimum over Fintype (12 messages, latest: Dec 18 2023 at 17:44)
• prodZeroRing vs prodUnique (7 messages, latest: Dec 18 2023 at 14:28)
• Working on Lindelöf spaces (4 messages, latest: Dec 18 2023 at 13:40)
• Renaming monotonicity of powers lemmas (7 messages, latest: Dec 18 2023 at 08:35)
• Topology on sets with manifold structure (9 messages, latest: Dec 18 2023 at 06:42)
• Avoiding type annotation (47 messages, latest: Dec 17 2023 at 13:37)
• naming conventions (292 messages, latest: Dec 16 2023 at 19:32)
• github permission (228 messages, latest: Dec 16 2023 at 14:42)
• lift doesn't like metavariables (4 messages, latest: Dec 15 2023 at 18:21)
• Listable types (14 messages, latest: Dec 15 2023 at 17:15)
• tsum over equivalent (equal) subtypes (4 messages, latest: Dec 15 2023 at 15:39)
• simp? now produces fewer irrelevant lemmas (24 messages, latest: Dec 15 2023 at 15:20)
• SignType woes (29 messages, latest: Dec 15 2023 at 12:00)
• Declaration is not allowed to exist (19 messages, latest: Dec 15 2023 at 05:26)
• AbstractSimplicialComplex (22 messages, latest: Dec 14 2023 at 20:58)
• mathlib4 speedcenter (186 messages, latest: Dec 14 2023 at 15:22)
• Shrinking epsilon in analysis proofs (30 messages, latest: Dec 14 2023 at 15:15)
• ✔ #align move (14 messages, latest: Dec 14 2023 at 14:22)
• split/rename PowerSeries/Basic ? (4 messages, latest: Dec 14 2023 at 10:30)
• Could positivity handle sums of squares? (42 messages, latest: Dec 14 2023 at 05:23)
• Failures in Mathlib.Computability.Primrec after Std bump (3 messages, latest: Dec 14 2023 at 03:05)
• Spelling of well-ordered type (7 messages, latest: Dec 13 2023 at 11:46)
• Timeout in Submodule (𝓞 K) (𝓞 K) (11 messages, latest: Dec 13 2023 at 10:27)
• Some files not found in the cache (58 messages, latest: Dec 13 2023 at 07:35)
• Contributing sifted colimits (how to define them?) (15 messages, latest: Dec 12 2023 at 23:47)
• Complex.ext (18 messages, latest: Dec 12 2023 at 21:53)
• (deterministic) timeout at 'typeclass' for InvolutiveStar (18 messages, latest: Dec 12 2023 at 21:38)
• Contributing proof of Descartes' Rule of Signs (12 messages, latest: Dec 12 2023 at 17:02)
• norm_cast gives Int.subNatNat (4 messages, latest: Dec 12 2023 at 16:28)
• Push access (25 messages, latest: Dec 12 2023 at 15:34)
• ✔ Semrings to Rings and Categories (5 messages, latest: Dec 12 2023 at 14:03)
• Ordinals and fixed points of monotone functions (5 messages, latest: Dec 12 2023 at 12:05)
• lift unhappy with let or set values (9 messages, latest: Dec 11 2023 at 21:13)
• Naming around local homeomorphisms (8 messages, latest: Dec 11 2023 at 20:40)
• Strange Naming in Model Theory (3 messages, latest: Dec 11 2023 at 18:14)
• Addition on intervals? (29 messages, latest: Dec 11 2023 at 18:13)
• to_additive and other attributes (3 messages, latest: Dec 11 2023 at 11:57)
• generalize_proofs sometimes silently has no effect (2 messages, latest: Dec 11 2023 at 05:32)
• error building windows exe proj (64 messages, latest: Dec 11 2023 at 00:39)
• congr hogging up holes (3 messages, latest: Dec 10 2023 at 18:53)
• New by_approx tactic for proving real inequalities (3 messages, latest: Dec 10 2023 at 16:11)
• Noncommutative ring things (149 messages, latest: Dec 10 2023 at 10:14)
• Removing classicality from Finsupp.single and `Finsupp…. (20 messages, latest: Dec 09 2023 at 23:24)
• variable! (67 messages, latest: Dec 09 2023 at 14:13)
• Std bump mess (13 messages, latest: Dec 09 2023 at 05:34)
• linarith regression (14 messages, latest: Dec 08 2023 at 22:56)
• about PartENat (17 messages, latest: Dec 08 2023 at 00:50)
• extract_goal when the goal is False (12 messages, latest: Dec 07 2023 at 22:51)
• ring_nf returns ugly literals (35 messages, latest: Dec 07 2023 at 16:19)
• Pattern matching in set-builder notation (14 messages, latest: Dec 06 2023 at 18:56)
• Go to definition on congr(...) goes to the def of id (1 message, latest: Dec 06 2023 at 18:54)
• parsing Integer (2 messages, latest: Dec 06 2023 at 14:55)
• NonZeroDivisorLeft and NonZeroDivisor (1 message, latest: Dec 05 2023 at 18:07)
• unknown free variable in norm_num (2 messages, latest: Dec 05 2023 at 16:18)
• norm_num (45 messages, latest: Dec 05 2023 at 15:36)
• Help with complitacted induction proof (30 messages, latest: Dec 05 2023 at 15:33)
• help consumes next command (1 message, latest: Dec 05 2023 at 11:59)
• Typeclasses for reflecting order (9 messages, latest: Dec 05 2023 at 11:14)
• Why does norm_num simplify these two values? (2 messages, latest: Dec 05 2023 at 09:54)
• Generalizing Group Action (10 messages, latest: Dec 05 2023 at 08:34)
• Tactic for getting all hypotheses out of a finite forall (14 messages, latest: Dec 05 2023 at 07:35)
• Polynomial.aeval broke (13 messages, latest: Dec 04 2023 at 23:06)
• Proposed refactor of Bitvec (421 messages, latest: Dec 04 2023 at 18:07)
• writing lemmas about ofNat (53 messages, latest: Dec 04 2023 at 12:27)
• speedcenter on nightly-testing (8 messages, latest: Dec 04 2023 at 10:32)
• [rw at ](topic/rw.20at.20.html) (12 messages, latest: Dec 04 2023 at 08:48)
• gcongr speed (2 messages, latest: Dec 03 2023 at 17:08)
• addressing lean4#2220 (HPow elaboration) (10 messages, latest: Dec 03 2023 at 15:47)
• by_ contra and by_contra' (16 messages, latest: Dec 03 2023 at 05:48)
• Did norm_num just get weaker? (51 messages, latest: Dec 03 2023 at 05:40)
• gcongr and positivity in Tactic.Common (21 messages, latest: Dec 03 2023 at 05:15)
• exact? test failure: le_antisymm vs ge_antisymm (16 messages, latest: Dec 03 2023 at 01:18)
• Bench failed? (2 messages, latest: Dec 03 2023 at 01:13)
• Representatives of each part of a Finpartition (7 messages, latest: Dec 02 2023 at 15:49)
• bump/v4.4.0 (10 messages, latest: Dec 02 2023 at 08:46)
• new release (6 messages, latest: Dec 02 2023 at 00:38)
• Weird behavior with Function.comp with and without Mathlib (10 messages, latest: Dec 01 2023 at 23:35)
• Unicode combining over arrows (11 messages, latest: Dec 01 2023 at 21:52)
• Field names collision for type class inheritance (7 messages, latest: Dec 01 2023 at 21:16)
• zmod decidability (6 messages, latest: Dec 01 2023 at 19:08)
• Defining a Finpartition from a Setoid over a Fintype (19 messages, latest: Dec 01 2023 at 16:39)
• PNat powers in a semigroup (31 messages, latest: Dec 01 2023 at 09:30)
• Finset.choose (13 messages, latest: Dec 01 2023 at 04:14)
• Obscure test fail (61 messages, latest: Dec 01 2023 at 03:37)
• Codegen can't support recursor (7 messages, latest: Dec 01 2023 at 00:30)
• lake exe cache get errors (209 messages, latest: Dec 01 2023 at 00:16)
• Naming convention (406 messages, latest: Nov 30 2023 at 16:57)
• Cotransitivity (1 message, latest: Nov 30 2023 at 16:17)
• Preferred spelling of cancellative semigroups (8 messages, latest: Nov 30 2023 at 16:14)
• Weird git behavior (9 messages, latest: Nov 30 2023 at 15:03)
• scoped simp and to_additive (4 messages, latest: Nov 30 2023 at 14:57)
• ✔ Problem with coercions (5 messages, latest: Nov 30 2023 at 12:02)
• ✔ Graph of algebraic classes (6 messages, latest: Nov 30 2023 at 10:41)
• instance graphs (2 messages, latest: Nov 30 2023 at 10:40)
• Nat.dvd_mul and simp (32 messages, latest: Nov 30 2023 at 01:38)
• Std bump (2 messages, latest: Nov 29 2023 at 22:52)
• From Pmf to Expectations (15 messages, latest: Nov 29 2023 at 08:31)
• simp_rw vs simp only (8 messages, latest: Nov 29 2023 at 04:50)
• rewrite_search (117 messages, latest: Nov 28 2023 at 23:03)
• Importing Mathlib breaks simp_arith (19 messages, latest: Nov 28 2023 at 19:44)
• ✔ Function.swap notation (3 messages, latest: Nov 28 2023 at 19:26)
• Return type in FunLike.coe not beta reduced (2 messages, latest: Nov 28 2023 at 19:25)
• Why is arithmetic in ℚ irreducible? (1 message, latest: Nov 27 2023 at 01:25)
• fin_cases doesn't come up in mathlib4 doc search (5 messages, latest: Nov 26 2023 at 14:26)
• measurability tactic times out on Prod.fst \circ Prod.fst (17 messages, latest: Nov 26 2023 at 14:26)
• Automating proofs for computability (3 messages, latest: Nov 26 2023 at 14:20)
• Waiting for nightly-testing-2023-11-24 (10 messages, latest: Nov 26 2023 at 04:42)
• Download oleans that are bitwise identical? (16 messages, latest: Nov 24 2023 at 19:12)
• Spelling of Subtype.val in LinearIndependent (63 messages, latest: Nov 24 2023 at 12:12)
• ✔ Lifting ZMOD to char p ring (5 messages, latest: Nov 24 2023 at 08:09)
• ✔ Reverse of mod_add_div (3 messages, latest: Nov 24 2023 at 08:09)
• hint tactic priorities (31 messages, latest: Nov 23 2023 at 21:11)
• tactic to destructure under certain conditions? (20 messages, latest: Nov 23 2023 at 00:58)
• mathlib4_docs builds are failing (4 messages, latest: Nov 23 2023 at 00:00)
• Creating projects (2 messages, latest: Nov 22 2023 at 23:50)
• refine vs refine' (64 messages, latest: Nov 22 2023 at 20:46)
• Definition of module (13 messages, latest: Nov 22 2023 at 08:31)
• linarith bug with metavariable (11 messages, latest: Nov 21 2023 at 23:46)
• Grassmannians (67 messages, latest: Nov 21 2023 at 18:19)
• Bringing back ⇑ (33 messages, latest: Nov 21 2023 at 15:36)
• Why Vector is defined as a List subtype (8 messages, latest: Nov 21 2023 at 11:14)
• autocomplete help for options (14 messages, latest: Nov 21 2023 at 08:49)
• Definition of pdf as rnDeriv (19 messages, latest: Nov 20 2023 at 21:57)
• by_casesusing the default argument (20 messages, latest: Nov 20 2023 at 19:15)
• PR Permission (2 messages, latest: Nov 20 2023 at 17:31)
• non-GMP bignums (8 messages, latest: Nov 20 2023 at 17:08)
• Proving the value of exp (S_5) (39 messages, latest: Nov 20 2023 at 16:53)
• simp? giving nonsense lemmas (36 messages, latest: Nov 20 2023 at 16:41)
• simps question (2 messages, latest: Nov 20 2023 at 13:08)
• HPow bug again (2 messages, latest: Nov 20 2023 at 09:29)
• Hermite's theorem on number fields (7 messages, latest: Nov 20 2023 at 08:43)
• 10^40000000 = 10^40000000 := by norm_num (31 messages, latest: Nov 20 2023 at 04:21)
• LaTeX problem in docstring (13 messages, latest: Nov 19 2023 at 20:54)
• Linting for bad instances (4 messages, latest: Nov 19 2023 at 18:55)
• polyrith does not work in the web editor (1 message, latest: Nov 19 2023 at 18:50)
• Rewrite with inequalities (91 messages, latest: Nov 18 2023 at 22:28)
• Crazy rcases success (5 messages, latest: Nov 18 2023 at 21:05)
• Help with an arithmetic lemma (22 messages, latest: Nov 18 2023 at 16:21)
• aesop vs solve_by_elim for continuity tactic (13 messages, latest: Nov 18 2023 at 14:21)
• pow_eq_one_iff_of_nonneg (5 messages, latest: Nov 18 2023 at 11:16)
• Time to compile Mathlib on M3 ? (11 messages, latest: Nov 18 2023 at 08:34)
• abel and progress (3 messages, latest: Nov 18 2023 at 02:07)
• Test do not use lakefile config (9 messages, latest: Nov 18 2023 at 00:57)
• Citing the conceptual framework of Mathlib (4 messages, latest: Nov 18 2023 at 00:21)
• hint tactic (12 messages, latest: Nov 17 2023 at 13:00)
• Argument order inconsistent in Has(M)FDerivAt (2 messages, latest: Nov 17 2023 at 11:27)
• Regression in simp (64 messages, latest: Nov 17 2023 at 10:02)
• apply? failure (14 messages, latest: Nov 17 2023 at 06:54)
• Exact? fails on le_antisymm (4 messages, latest: Nov 17 2023 at 03:51)
• Matching compositions with Qq (33 messages, latest: Nov 17 2023 at 02:08)
• to_additive interaction with strings and syntax highlight (5 messages, latest: Nov 16 2023 at 17:37)
• bug in mathlib's have extension (15 messages, latest: Nov 16 2023 at 16:49)
• Should the cast to ContinuousOpenMap be a @\[coe\] def? (3 messages, latest: Nov 16 2023 at 14:57)
• Differentiability of paths in manifolds (10 messages, latest: Nov 16 2023 at 12:30)
• LinearEquiv.finrank_eq : typeclass instance problem is stuck (12 messages, latest: Nov 16 2023 at 12:18)
• linarith fails in a simple example (47 messages, latest: Nov 16 2023 at 08:42)
• Real.exp (103 messages, latest: Nov 16 2023 at 03:23)
• Multiplicative doesn't play well with simp (12 messages, latest: Nov 16 2023 at 02:32)
• Should Subtype.val '' be related to Lean's internal cast? (37 messages, latest: Nov 15 2023 at 17:31)
• Cannot Find Real.add (33 messages, latest: Nov 15 2023 at 13:08)
• lake update: invalid toolchain name (19 messages, latest: Nov 15 2023 at 09:09)
• intervalIntegral.integral_const_mul is not a good simp lemma (6 messages, latest: Nov 14 2023 at 16:48)
• OrderedCancelCommMonoid extends (11 messages, latest: Nov 14 2023 at 14:56)
• fin_cases slow?! (23 messages, latest: Nov 14 2023 at 14:12)
• Relclasses instances (3 messages, latest: Nov 14 2023 at 10:33)
• v4.3.0-rc2 - comp_def and #8023 (73 messages, latest: Nov 14 2023 at 04:02)
• Disable lake post-hook when importing mathlib? (12 messages, latest: Nov 13 2023 at 23:09)
• type synonym or one field structure? (8 messages, latest: Nov 13 2023 at 19:09)
• Unhelpful error message (8 messages, latest: Nov 13 2023 at 16:52)
• Cannot use Nat.ModEq.pow_totient (Euler's theorem) (4 messages, latest: Nov 13 2023 at 15:20)
• Mathlib.Analysis.PSeries and HPow (5 messages, latest: Nov 13 2023 at 12:37)
• MeasureSpace instance on Subtype (5 messages, latest: Nov 13 2023 at 11:22)
• v4.3.0-rc2 (40 messages, latest: Nov 13 2023 at 10:45)
• Bad CoeFun instances on FiniteMeasure and ProbabilityMeasure (5 messages, latest: Nov 13 2023 at 09:47)
• IsLittleO as Tendsto (3 messages, latest: Nov 13 2023 at 05:05)
• Slow typechecking at rewrite (4 messages, latest: Nov 13 2023 at 03:00)
• refine? (4 messages, latest: Nov 12 2023 at 10:12)
• Pretty-print mvars without .1234? (9 messages, latest: Nov 12 2023 at 07:58)
• convert … using … with … (5 messages, latest: Nov 11 2023 at 21:29)
• ZMod 0 (12 messages, latest: Nov 11 2023 at 19:38)
• Re-using a branch for a new PR? (2 messages, latest: Nov 11 2023 at 19:28)
• Funlike (1 message, latest: Nov 11 2023 at 17:21)
• How can one prove a simple (in)equality in reals? (4 messages, latest: Nov 11 2023 at 13:06)
• [beginner] Failing to apply finsum_congr (8 messages, latest: Nov 11 2023 at 10:12)
• No space left on device (4 messages, latest: Nov 11 2023 at 07:31)
• exact? failing to find a lemma which closes the goal (11 messages, latest: Nov 11 2023 at 07:26)
• New fields in MetricSpace (19 messages, latest: Nov 11 2023 at 06:19)
• writing a positivity extension (10 messages, latest: Nov 11 2023 at 01:05)
• Klein 4 group PR relying on decide := true for simp (7 messages, latest: Nov 11 2023 at 00:31)
• run linters locally (9 messages, latest: Nov 10 2023 at 21:11)
• ✔ Cast to Fraction Ring (11 messages, latest: Nov 10 2023 at 18:59)
• ✔ Polynomial.coeff example (30 messages, latest: Nov 10 2023 at 15:29)
• rw? does not find lemma (10 messages, latest: Nov 10 2023 at 14:16)
• Slow rfl / Nat.log (7 messages, latest: Nov 10 2023 at 09:33)
• kernel metavariable bug (6 messages, latest: Nov 10 2023 at 03:45)
• upstreaming simps to Std (39 messages, latest: Nov 10 2023 at 01:55)
• Regression in continuity (33 messages, latest: Nov 09 2023 at 19:13)
• Why doesn't this work for ℝ? (5 messages, latest: Nov 09 2023 at 09:21)
• horner form in ring_nf (3 messages, latest: Nov 09 2023 at 03:18)
• ambiguous rewrite when only one is valid (5 messages, latest: Nov 09 2023 at 01:26)
• warning: expanding binder collection (17 messages, latest: Nov 08 2023 at 22:03)
• mathlib vs the literature (23 messages, latest: Nov 08 2023 at 18:52)
• aesop in Mathlib (9 messages, latest: Nov 08 2023 at 11:37)
• Lean extension reverts mathlib version (51 messages, latest: Nov 08 2023 at 02:25)
• Link to mathlib(3) in "How to contribute to mathlib" (2 messages, latest: Nov 07 2023 at 23:00)
• Groupoid.toCategory (9 messages, latest: Nov 07 2023 at 22:26)
• LinearOrder infer incorrect instance (12 messages, latest: Nov 07 2023 at 21:45)
• Where to put notation for orthogonality (23 messages, latest: Nov 07 2023 at 06:07)
• List.rdrop (8 messages, latest: Nov 07 2023 at 04:34)
• fatal: Needed a single revision (3 messages, latest: Nov 07 2023 at 04:12)
• List of linters (16 messages, latest: Nov 07 2023 at 01:23)
• ₓ in #align #5847 (10 messages, latest: Nov 06 2023 at 23:14)
• simpNF linter complains about a rfl lemma (3 messages, latest: Nov 06 2023 at 20:40)
• Another kind of simp regression (10 messages, latest: Nov 06 2023 at 18:32)
• out-of-date pull request (13 messages, latest: Nov 06 2023 at 14:01)
• References in QuadraticForm and CliffordAlgebra.Contraction (10 messages, latest: Nov 06 2023 at 11:56)
• Unecessarily complex goal (1 message, latest: Nov 06 2023 at 11:20)
• Coxeter Groups (53 messages, latest: Nov 06 2023 at 09:21)
• zify broken? (12 messages, latest: Nov 06 2023 at 09:06)
• adding imports breaks class inference? (7 messages, latest: Nov 06 2023 at 07:55)
• PDA (3 messages, latest: Nov 06 2023 at 07:10)
• Unused variable linter (6 messages, latest: Nov 06 2023 at 05:03)
• exact?% (22 messages, latest: Nov 06 2023 at 02:36)
• Generalising lemma for instances (26 messages, latest: Nov 05 2023 at 23:58)
• Problem in conv (11 messages, latest: Nov 05 2023 at 23:25)
• Define complex (path) integrals (6 messages, latest: Nov 05 2023 at 13:07)
• Stream' is inefficient (22 messages, latest: Nov 05 2023 at 12:36)
• Documented type for Finset.sum_range etc. (10 messages, latest: Nov 04 2023 at 23:22)
• simpa? "Try this" not clickable (2 messages, latest: Nov 04 2023 at 17:41)
• How to install mathlib4 (20 messages, latest: Nov 04 2023 at 14:38)
• Rearranging sums (8 messages, latest: Nov 04 2023 at 02:45)
• norm_cast and ofNat (14 messages, latest: Nov 03 2023 at 18:28)
• BigOperators theorems for Multiset (11 messages, latest: Nov 03 2023 at 18:25)
• Sqrt notation typeclass (7 messages, latest: Nov 03 2023 at 18:10)
• dot notation with Multiplicative (7 messages, latest: Nov 03 2023 at 14:42)
• trans vs trans (2 messages, latest: Nov 03 2023 at 07:59)
• norm_num extensions (15 messages, latest: Nov 03 2023 at 00:26)
• tactic request: Nat.cast to ofNat (1 message, latest: Nov 02 2023 at 23:46)
• Citing Mathlib 4 (4 messages, latest: Nov 02 2023 at 23:18)
• Dealing with multiple instances on a single type (4 messages, latest: Nov 02 2023 at 20:09)
• ✔ request for help with lake build failing (4 messages, latest: Nov 02 2023 at 18:06)
• request for help with failure in Archive (10 messages, latest: Nov 02 2023 at 16:16)
• aesop_graph vs aesop (16 messages, latest: Nov 02 2023 at 11:15)
• Prove algebraic class of subtype via closure (5 messages, latest: Nov 02 2023 at 11:06)
• ✔ Dinatural transformations (6 messages, latest: Nov 02 2023 at 11:03)
• preferred spelling (9 messages, latest: Nov 02 2023 at 10:59)
• avoid expansion of class fields (10 messages, latest: Nov 02 2023 at 10:04)
• Compiler IR Check Failed vs Failed to compile Definition (2 messages, latest: Nov 02 2023 at 07:33)
• Topology on Lp (38 messages, latest: Nov 02 2023 at 03:35)
• request for help with filter notation (10 messages, latest: Nov 02 2023 at 02:40)
• Multiplicative mul and pow are wrong (7 messages, latest: Nov 01 2023 at 22:45)
• scoped notation3 (5 messages, latest: Nov 01 2023 at 19:48)
• Mismatched lattice instances? (7 messages, latest: Nov 01 2023 at 19:34)
• Reorganizing Mathlib.Algebra.Hom (9 messages, latest: Nov 01 2023 at 17:30)
• gcongr doc (7 messages, latest: Nov 01 2023 at 02:35)
• Complete Ordered AddCommMonoid (25 messages, latest: Nov 01 2023 at 01:56)
• Notation g^n incurs two slow CoeTs (3 messages, latest: Nov 01 2023 at 01:22)
• Crazy unification quests (8 messages, latest: Oct 31 2023 at 23:12)
• HaveIin statements/proofs (21 messages, latest: Oct 31 2023 at 19:37)
• A specific file triggers rpc errors (13 messages, latest: Oct 31 2023 at 18:30)
• ✔ How to do induction on a function with termination_by (3 messages, latest: Oct 31 2023 at 10:30)
• lake exe cache get (200 messages, latest: Oct 31 2023 at 08:56)
• Nonparametric induction (2 messages, latest: Oct 31 2023 at 06:54)
• n composable morphisms (25 messages, latest: Oct 31 2023 at 04:30)
• measurability regression (4 messages, latest: Oct 30 2023 at 19:09)
• Help with numerical computation (19 messages, latest: Oct 30 2023 at 14:03)
• No ⟦x⟧ notation in infoview? (7 messages, latest: Oct 29 2023 at 22:49)
• simp_all out of control (11 messages, latest: Oct 29 2023 at 18:22)
• small TODOs (7 messages, latest: Oct 29 2023 at 16:56)
• positivity regression (36 messages, latest: Oct 29 2023 at 15:31)
• exact? does not find default instances (4 messages, latest: Oct 29 2023 at 13:25)
• std4#183, lemmas about Bool (13 messages, latest: Oct 29 2023 at 13:23)
• nth_rw broken? (4 messages, latest: Oct 29 2023 at 10:50)
• using Iff rfl proofs in dsimp (31 messages, latest: Oct 28 2023 at 23:22)
• field_simp discharger (1 message, latest: Oct 28 2023 at 21:30)
• simp hangs forever (3 messages, latest: Oct 28 2023 at 18:22)
• How many of these topology lemmas are new? (25 messages, latest: Oct 28 2023 at 05:09)
• The ring expression types (4 messages, latest: Oct 28 2023 at 04:39)
• x ^ 2 defeq (15 messages, latest: Oct 27 2023 at 23:17)
• zify! (1 message, latest: Oct 27 2023 at 20:46)
• push_neg doesn't simplify fully (7 messages, latest: Oct 27 2023 at 19:05)
• Conflicting (?) Abs instances (7 messages, latest: Oct 27 2023 at 15:14)
• linarith max (7 messages, latest: Oct 27 2023 at 13:51)
• aesop change breaking Mathlib (6 messages, latest: Oct 27 2023 at 10:24)
• ✔ Selection Sort (69 messages, latest: Oct 27 2023 at 07:50)
• bug in convert (48 messages, latest: Oct 26 2023 at 23:41)
• Dealing with multiple goals (15 messages, latest: Oct 26 2023 at 20:35)
• continuity? says rename_i (7 messages, latest: Oct 26 2023 at 20:26)
• order and leading coefficient of analytic functions (3 messages, latest: Oct 26 2023 at 20:12)
• github projects (26 messages, latest: Oct 26 2023 at 14:33)
• Incompatible notations (8 messages, latest: Oct 26 2023 at 10:40)
• bug in replace (3 messages, latest: Oct 26 2023 at 01:19)
• Constructing a proof for Polynomial.IsRoot (18 messages, latest: Oct 25 2023 at 18:57)
• exact? in term mode (5 messages, latest: Oct 25 2023 at 18:24)
• !bench against commit? (18 messages, latest: Oct 25 2023 at 17:48)
• pp.beta, linter, "cannot evaluate … in the same module" (9 messages, latest: Oct 25 2023 at 16:25)
• SetLike coe to type display (13 messages, latest: Oct 25 2023 at 15:56)
• Splitting Topology/Connected.lean? (16 messages, latest: Oct 25 2023 at 11:45)
• Ring tactic on (n+1)^2=n^2+2n+1 (42 messages, latest: Oct 25 2023 at 08:48)
• Complex.sqrt (42 messages, latest: Oct 25 2023 at 05:40)
• beta_reduce (3 messages, latest: Oct 25 2023 at 03:16)
• phantom declaration (26 messages, latest: Oct 25 2023 at 03:15)
• ProofWidgets bump required (36 messages, latest: Oct 24 2023 at 17:00)
• fixes to simp regressions (24 messages, latest: Oct 24 2023 at 12:50)
• Regression in simp because of missing congr (8 messages, latest: Oct 24 2023 at 08:54)
• root names (44 messages, latest: Oct 24 2023 at 05:25)
• linarith does not know trichotomy? (3 messages, latest: Oct 24 2023 at 03:15)
• infinite loop in CI: get cache (15 messages, latest: Oct 24 2023 at 02:20)
• regression in rw (10 messages, latest: Oct 23 2023 at 17:44)
• CI "check for noisy stdout lines" (3 messages, latest: Oct 23 2023 at 14:57)
• FreeAlgebra.Rel (9 messages, latest: Oct 23 2023 at 08:36)
• !bench failed during download of pr release (6 messages, latest: Oct 23 2023 at 08:13)
• simp on binders (10 messages, latest: Oct 22 2023 at 23:13)
• SignType.sign vs Real.sign (9 messages, latest: Oct 22 2023 at 21:56)
• What kind of contributions should go to mathlib? (11 messages, latest: Oct 22 2023 at 21:52)
• Why are two rings needed here? (3 messages, latest: Oct 22 2023 at 20:29)
• weird performance of norm_num with Nat.digits (27 messages, latest: Oct 22 2023 at 19:27)
• Slow refine for ZMod (5 messages, latest: Oct 22 2023 at 16:09)
• brute force calculation of Bell/Stirling numbers (81 messages, latest: Oct 22 2023 at 10:19)
• gcongr handling equality? (17 messages, latest: Oct 22 2023 at 07:37)
• Why does gcongr hide variables? (6 messages, latest: Oct 22 2023 at 04:54)
• Build issue in CI (5 messages, latest: Oct 21 2023 at 19:13)
• use bug (27 messages, latest: Oct 21 2023 at 15:47)
• Decidable PythagoreanTriple (26 messages, latest: Oct 21 2023 at 13:13)
• says (6 messages, latest: Oct 21 2023 at 09:16)
• MaxCut by argmin (1 message, latest: Oct 21 2023 at 07:44)
• rintro? (2 messages, latest: Oct 21 2023 at 03:19)
• PR associated with default branch (3 messages, latest: Oct 20 2023 at 17:27)
• whnf bug 2 (16 messages, latest: Oct 20 2023 at 16:08)
• aesop for SetLike (57 messages, latest: Oct 20 2023 at 16:08)
• Convexity refactor (69 messages, latest: Oct 20 2023 at 15:37)
• Showing off mathlib in talks (3 messages, latest: Oct 20 2023 at 12:38)
• docstring linter and where-definitions (5 messages, latest: Oct 20 2023 at 11:12)
• reviewdog (38 messages, latest: Oct 20 2023 at 10:34)
• norm_num on Fin (11 messages, latest: Oct 20 2023 at 08:27)
• Tactic state explosion (27 messages, latest: Oct 19 2023 at 21:30)
• RingHomProperties (34 messages, latest: Oct 19 2023 at 14:20)
• regression in linear_combination (30 messages, latest: Oct 19 2023 at 01:51)
• Vectors/n-tuples (2 messages, latest: Oct 18 2023 at 23:28)
• Instance inference error (8 messages, latest: Oct 18 2023 at 20:20)
• simp vs rw again (31 messages, latest: Oct 18 2023 at 19:54)
• lake update reordering dependencies in manifest (3 messages, latest: Oct 18 2023 at 18:03)
• Why does rw not rewrite inside quantifiers? (7 messages, latest: Oct 18 2023 at 15:40)
• Strange recursion depth error (9 messages, latest: Oct 18 2023 at 13:27)
• Docs "#" in math mode errors (5 messages, latest: Oct 18 2023 at 13:24)
• Strange field_simp failure (86 messages, latest: Oct 18 2023 at 13:06)
• Finset in mathlib4_docs (8 messages, latest: Oct 18 2023 at 07:35)
• nonterminal simp then rfl (14 messages, latest: Oct 18 2023 at 06:29)
• lake exe graph (93 messages, latest: Oct 18 2023 at 06:27)
• ✔ Trouble with sInf (10 messages, latest: Oct 18 2023 at 04:43)
• ✔ UpperCamelCase forCoeFun α (fun _ : β => Type*) #7526 (17 messages, latest: Oct 18 2023 at 02:19)
• Elementary functions (10 messages, latest: Oct 17 2023 at 05:16)
• cases exposes type (10 messages, latest: Oct 16 2023 at 20:38)
• Why is CI lint so slow? (7 messages, latest: Oct 16 2023 at 13:07)
• Using finishing tactics inside aesop (13 messages, latest: Oct 16 2023 at 11:02)
• Bounded Fintype (9 messages, latest: Oct 16 2023 at 10:18)
• add_comm without add_assoc (10 messages, latest: Oct 15 2023 at 11:29)
• Logical congruence or weakening tactic (59 messages, latest: Oct 15 2023 at 08:38)
• Update std for lean4-pr-testing branches? (3 messages, latest: Oct 15 2023 at 05:37)
• Ensuring a repo builds on top of mathlib PRs (13 messages, latest: Oct 14 2023 at 23:57)
• induction' leaving junk (8 messages, latest: Oct 14 2023 at 23:49)
• lake exe cache get should check toolchains (37 messages, latest: Oct 14 2023 at 10:30)
• WithBot manipulation? (7 messages, latest: Oct 13 2023 at 23:34)
• ✔ AE(Strongly)Measurable assumption (13 messages, latest: Oct 13 2023 at 22:57)
• TensorProduct.lift - noncomputable (21 messages, latest: Oct 13 2023 at 19:09)
• define gradient of scalar-valued function on a Hilbert space (38 messages, latest: Oct 13 2023 at 13:01)
• Line-wrapping of infix operators (1 message, latest: Oct 13 2023 at 11:48)
• Formal power series on ι -> R (24 messages, latest: Oct 13 2023 at 11:42)
• ✔ Representing Interval Partitions (25 messages, latest: Oct 13 2023 at 08:17)
• ✔ Card of Finset (4 messages, latest: Oct 13 2023 at 02:11)
• ✔ Goal not closing when importing (8 messages, latest: Oct 12 2023 at 23:08)
• ✔ Trouble with type-casting complex numbers (5 messages, latest: Oct 12 2023 at 20:23)
• Quotient.mk vs .mk' vs .mk'' (34 messages, latest: Oct 12 2023 at 19:58)
• ModuleCat.mk slowness (28 messages, latest: Oct 12 2023 at 19:56)
• let vs letI for local instances (12 messages, latest: Oct 12 2023 at 10:22)
• Difference between ∑ᶠ and ∑' (5 messages, latest: Oct 12 2023 at 03:13)
• Moving lean3 project to lean4 (12 messages, latest: Oct 11 2023 at 20:08)
• Trouble with sets (6 messages, latest: Oct 11 2023 at 20:01)
• #7584 speed up Ideal.Quotient.commRing instance (16 messages, latest: Oct 11 2023 at 13:46)
• Measure on an infinite product (8 messages, latest: Oct 11 2023 at 12:44)
• Naming convention: topological spaces (26 messages, latest: Oct 11 2023 at 12:32)
• Functions and prob. distributions (1 message, latest: Oct 11 2023 at 09:11)
• Fintype.card and subgroups (18 messages, latest: Oct 10 2023 at 21:16)
• toFinsetFactors (18 messages, latest: Oct 10 2023 at 15:25)
• aroots (62 messages, latest: Oct 10 2023 at 14:34)
• CI failure when building MathlibExtras (123 messages, latest: Oct 09 2023 at 20:57)
• missing Decidable instances (21 messages, latest: Oct 09 2023 at 17:10)
• instance names (88 messages, latest: Oct 09 2023 at 16:31)
• Tests for the polyrith tactic (1 message, latest: Oct 09 2023 at 16:27)
• linarith application type mismatch (8 messages, latest: Oct 09 2023 at 11:24)
• ✔ LinearOrder additionally specified (13 messages, latest: Oct 09 2023 at 11:20)
• coe confusion (21 messages, latest: Oct 09 2023 at 08:08)
• ✔ Location of Module.Finite (4 messages, latest: Oct 08 2023 at 18:26)
• ✔ Function to remove at most one element from a List. (17 messages, latest: Oct 08 2023 at 10:02)
• project management (15 messages, latest: Oct 08 2023 at 03:32)
• Minimum of a finite set (12 messages, latest: Oct 07 2023 at 23:16)
• Mathlib Global Installation (38 messages, latest: Oct 06 2023 at 21:23)
• Specific typeclasses alternative (41 messages, latest: Oct 06 2023 at 14:35)
• ✔ simp fail with Classical.choose (10 messages, latest: Oct 06 2023 at 10:14)
• coprime ideal (68 messages, latest: Oct 06 2023 at 07:58)
• cobounded vs cocompact (6 messages, latest: Oct 05 2023 at 23:28)
• Select and insert widgets (25 messages, latest: Oct 05 2023 at 14:04)
• Amenable group actions (81 messages, latest: Oct 05 2023 at 13:16)
• Random AG failure (20 messages, latest: Oct 05 2023 at 13:01)
• ✔ lint style (bors/CI) (4 messages, latest: Oct 05 2023 at 08:55)
• lean-pr-testing and cache (11 messages, latest: Oct 05 2023 at 06:16)
• induction' leaves junk around (1 message, latest: Oct 04 2023 at 23:48)
• Visualizing the algebra hierarchy (12 messages, latest: Oct 04 2023 at 22:37)
• Build failed: detect changes to header SHAs (29 messages, latest: Oct 04 2023 at 20:40)
• suppress_compilation (22 messages, latest: Oct 04 2023 at 15:39)
• RingCon algebraic TC instances (35 messages, latest: Oct 04 2023 at 12:48)
• unary function to (n=1)-ary (6 messages, latest: Oct 03 2023 at 16:25)
• ✔ Rat.abs name? (11 messages, latest: Oct 03 2023 at 16:14)
• Understanding to_additive (1 message, latest: Oct 02 2023 at 15:32)
• default induction (45 messages, latest: Oct 02 2023 at 13:53)
• ✔ Indirect indexing (4 messages, latest: Oct 02 2023 at 13:47)
• exact? and apply? high memory usage (6 messages, latest: Oct 02 2023 at 08:28)
• noncomputable and to_additive (4 messages, latest: Oct 01 2023 at 14:58)
• RFC: names for different bundlings of the same function (7 messages, latest: Oct 01 2023 at 13:22)
• ✔ group and borelize tactics (3 messages, latest: Sep 30 2023 at 16:34)
• Problem inferring usage of inf_le_left (40 messages, latest: Sep 30 2023 at 11:37)
• Generalizing some statements from fields to division rings (16 messages, latest: Sep 29 2023 at 20:00)
• Qq error in MOP update (25 messages, latest: Sep 29 2023 at 16:57)
• split AlgebraicGeometry (15 messages, latest: Sep 29 2023 at 07:46)
• prop valued ifs (11 messages, latest: Sep 28 2023 at 14:04)
• Removing Nat.bitwise' in favor of Nat.bitwise (13 messages, latest: Sep 28 2023 at 11:44)
• IsROrC vs Complex (14 messages, latest: Sep 28 2023 at 04:48)
• More stuff on model theory (3 messages, latest: Sep 28 2023 at 00:45)
• rotate (138 messages, latest: Sep 27 2023 at 20:28)
• TFAE.out in rw (2 messages, latest: Sep 27 2023 at 19:51)
• Verbose failing simpa? (1 message, latest: Sep 27 2023 at 15:07)
• !4#4183 simps maximum recursion depth (8 messages, latest: Sep 27 2023 at 14:42)
• simp fails with "failed to synthesize Subsingleton" (14 messages, latest: Sep 27 2023 at 07:58)
• What is wrong with RingTheory.Kaehler? (30 messages, latest: Sep 27 2023 at 06:21)
• Promoting to polymorphic (4 messages, latest: Sep 26 2023 at 17:52)
• thoughts on gradient (40 messages, latest: Sep 26 2023 at 13:01)
• montgomery reduction proof – would love some feedback! (17 messages, latest: Sep 26 2023 at 08:57)
• duplicate notation cexp (10 messages, latest: Sep 25 2023 at 21:38)
• style for proofs with \|. (17 messages, latest: Sep 25 2023 at 18:37)
• Real^Nat should not be interpreted as Real^Real (4 messages, latest: Sep 24 2023 at 23:31)
• Fin DecidableEq diamond (10 messages, latest: Sep 24 2023 at 22:32)
• How to sharpen an off-by-one (3 messages, latest: Sep 24 2023 at 15:49)
• Projective space (52 messages, latest: Sep 24 2023 at 03:48)
• Orange bar hell even after after cache get (12 messages, latest: Sep 23 2023 at 13:58)
• exact? and this (55 messages, latest: Sep 22 2023 at 03:40)
• naming in docs#SubsetProperties (12 messages, latest: Sep 21 2023 at 15:18)
• docBlame (48 messages, latest: Sep 21 2023 at 14:03)
• Computable degree-bound polynomials (52 messages, latest: Sep 21 2023 at 11:14)
• lake exe cache get not producing a useful cache on gitpod (19 messages, latest: Sep 21 2023 at 11:08)
• Reordering arguments of Set.EqOn (25 messages, latest: Sep 21 2023 at 05:01)
• doc-gen and ProofWidgets (6 messages, latest: Sep 20 2023 at 20:04)
• lake exe cache get broken (28 messages, latest: Sep 20 2023 at 17:20)
• ✔ pre-built release assets for windows (59 messages, latest: Sep 20 2023 at 02:35)
• (1 2 3 4)^4 = 1 is slow (3 messages, latest: Sep 19 2023 at 23:24)
• List insertion slowdown (17 messages, latest: Sep 19 2023 at 20:44)
• lemma vs theorem (174 messages, latest: Sep 19 2023 at 16:05)
• Scope of mathlib (2 messages, latest: Sep 19 2023 at 14:55)
• ✔ Strange linarith behavior (18 messages, latest: Sep 19 2023 at 13:32)
• rw? not closing goal (14 messages, latest: Sep 19 2023 at 11:41)
• Bounded vs BddAbove (10 messages, latest: Sep 19 2023 at 06:12)
• efficiently dealing with / vs .div (18 messages, latest: Sep 19 2023 at 03:31)
• Slow coercion from Fin n to Fin m (10 messages, latest: Sep 18 2023 at 15:38)
• questions about Rat.isInt (25 messages, latest: Sep 18 2023 at 10:28)
• ConeMorphism.Hom (7 messages, latest: Sep 18 2023 at 07:50)
• borelize gives "failed to create binder…" (29 messages, latest: Sep 18 2023 at 06:00)
• bors changed base branch (58 messages, latest: Sep 18 2023 at 01:10)
• gcongr and notation (14 messages, latest: Sep 17 2023 at 21:42)
• Weird lemmas shown in docgen (2 messages, latest: Sep 17 2023 at 20:11)
• Variable expansion in filter_upwards (10 messages, latest: Sep 17 2023 at 18:22)
• root.trans vs. Trans.trans (8 messages, latest: Sep 17 2023 at 15:24)
• Pretty printing beta reduction (36 messages, latest: Sep 17 2023 at 15:12)
• bump to v4.1.0-rc1 (23 messages, latest: Sep 17 2023 at 11:26)
• Pretty printing proofs.WithType (4 messages, latest: Sep 16 2023 at 12:33)
• ✔ mismatch Monotone after Set.restrict (23 messages, latest: Sep 16 2023 at 09:15)
• suffices whinge (63 messages, latest: Sep 15 2023 at 20:02)
• simp? failure (4 messages, latest: Sep 15 2023 at 13:26)
• Spelling congrArg or congr_arg (64 messages, latest: Sep 15 2023 at 12:13)
• Pmf: ENNReal vs. NNReal (21 messages, latest: Sep 15 2023 at 10:10)
• Quotienting by a polynomial (14 messages, latest: Sep 14 2023 at 19:37)
• Elgot monads (1 message, latest: Sep 14 2023 at 19:04)
• Z / q.Z (23 messages, latest: Sep 14 2023 at 18:58)
• Monoid coproduct (9 messages, latest: Sep 14 2023 at 18:03)
• congr' (3 messages, latest: Sep 14 2023 at 17:34)
• naming conventions: natCast vs nat_cast (39 messages, latest: Sep 14 2023 at 12:38)
• ✔ lint mathlib fail (18 messages, latest: Sep 14 2023 at 09:06)
• CompLemmas (5 messages, latest: Sep 14 2023 at 09:05)
• simp loop (15 messages, latest: Sep 14 2023 at 08:52)
• Notation introduces sorry (29 messages, latest: Sep 13 2023 at 13:04)
• ✔ structure and cases (5 messages, latest: Sep 13 2023 at 12:48)
• Integral notation (123 messages, latest: Sep 13 2023 at 04:14)
• New exotic simp failure (22 messages, latest: Sep 12 2023 at 20:15)
• Sup is not longer Sup (15 messages, latest: Sep 12 2023 at 17:33)
• running cache get as part of every lake build (107 messages, latest: Sep 12 2023 at 17:20)
• Search for actual match (16 messages, latest: Sep 12 2023 at 14:38)
• Weird error caused by instance (2 messages, latest: Sep 12 2023 at 13:02)
• GitHub: wrong blocked-by label from bot (2 messages, latest: Sep 12 2023 at 00:07)
• ✔ Overview of Mathlib4 (7 messages, latest: Sep 11 2023 at 21:37)
• doc lint on let rec? (7 messages, latest: Sep 11 2023 at 21:10)
• Lint fail: replace() takes no keyword arguments (8 messages, latest: Sep 11 2023 at 14:26)
• Debugging procedure (60 messages, latest: Sep 11 2023 at 12:23)
• mk_all.sh (141 messages, latest: Sep 11 2023 at 08:42)
• inherit_doc on projections (14 messages, latest: Sep 11 2023 at 08:25)
• Should we merge Quotient.out and Quotient.unquot? (44 messages, latest: Sep 10 2023 at 19:35)
• bug in #minimize_imports, vs. #redundant_imports (34 messages, latest: Sep 10 2023 at 10:46)
• Finset.filter_congr_decidable (6 messages, latest: Sep 09 2023 at 21:41)
• @[deriving …] –> ? (4 messages, latest: Sep 09 2023 at 14:58)
• deprecated lemma from rw? (7 messages, latest: Sep 08 2023 at 21:07)
• Trouble Importing Mathlib (11 messages, latest: Sep 08 2023 at 16:24)
• Ring instance (19 messages, latest: Sep 08 2023 at 15:08)
• mod lt possibly missing (4 messages, latest: Sep 07 2023 at 13:27)
• Naming of lemmas about / and % on Int (7 messages, latest: Sep 07 2023 at 12:06)
• Mathlib4 tactics list? (6 messages, latest: Sep 07 2023 at 06:07)
• HomClasses and tooling (9 messages, latest: Sep 06 2023 at 22:47)
• Type synonym boilerplate (10 messages, latest: Sep 06 2023 at 16:01)
• exact? recent regression? (14 messages, latest: Sep 05 2023 at 23:59)
• erasing unfold rules in aesop, and traceScript := true (8 messages, latest: Sep 05 2023 at 21:02)
• overwriting fields (12 messages, latest: Sep 05 2023 at 20:30)
• Continuous.pow not picked up by continuity (9 messages, latest: Sep 05 2023 at 16:38)
• Set.Accumulate (13 messages, latest: Sep 05 2023 at 12:54)
• condexp as a map between L¹s (7 messages, latest: Sep 05 2023 at 12:51)
• diagnosing timeouts in RingHom.RespectsIso.ofRestrict_mor… (12 messages, latest: Sep 05 2023 at 07:10)
• mathport and leanproject build (12 messages, latest: Sep 05 2023 at 05:52)
• ideas for speeding up CI (117 messages, latest: Sep 04 2023 at 23:37)
• Keyboard shortcut to apply first Try this: (7 messages, latest: Sep 04 2023 at 23:27)
• Nested binders without annotations (21 messages, latest: Sep 04 2023 at 23:23)
• Universe variables in mathlib docs have strange spaces (1 message, latest: Sep 04 2023 at 19:47)
• Some observations on eta experiment (102 messages, latest: Sep 04 2023 at 04:45)
• simpNF linter in #6931 (1 message, latest: Sep 03 2023 at 16:51)
• mathport experience (25 messages, latest: Sep 02 2023 at 20:09)
• red x (8 messages, latest: Sep 02 2023 at 07:37)
• fact_finiteDimensional_of_finrank_eq_succ (21 messages, latest: Sep 01 2023 at 20:57)
• falling factorial as polynomial (3 messages, latest: Sep 01 2023 at 13:12)
• ✔ 0 : Fin n (3 messages, latest: Sep 01 2023 at 08:37)
• unfold_coes (4 messages, latest: Sep 01 2023 at 03:13)
• Interval integral (13 messages, latest: Sep 01 2023 at 03:11)
• lookup3 alias issue? (4 messages, latest: Aug 31 2023 at 22:12)
• notation3 issue (4 messages, latest: Aug 31 2023 at 20:32)
• Slow SecondCountableEither (7 messages, latest: Aug 31 2023 at 20:21)
• Lean.Internal.CoeM (4 messages, latest: Aug 31 2023 at 15:43)
• Cartesian product of two Hilbert spaces (7 messages, latest: Aug 31 2023 at 14:17)
• Reducing mod n (31 messages, latest: Aug 30 2023 at 19:09)
• syntax for powers? (19 messages, latest: Aug 30 2023 at 12:52)
• lean-cache: lake exe cache rewrite (96 messages, latest: Aug 30 2023 at 12:32)
• Debugging typeclass inference (6 messages, latest: Aug 30 2023 at 11:06)
• to_additive and structure (5 messages, latest: Aug 30 2023 at 10:02)
• Redundant variable declaration (16 messages, latest: Aug 30 2023 at 09:47)
• Code action PANIC at Lean.Name.getString! (3 messages, latest: Aug 30 2023 at 09:04)
• ✔ Irrational in mathlib4 (5 messages, latest: Aug 30 2023 at 04:34)
• unusedVariables (101 messages, latest: Aug 30 2023 at 03:41)
• instructions for new project (45 messages, latest: Aug 29 2023 at 14:37)
• Mathlib4 porting meeting series (400 messages, latest: Aug 28 2023 at 20:44)
• Question about Elementary Geometry formalization (5 messages, latest: Aug 28 2023 at 20:23)
• test/change.lean (19 messages, latest: Aug 28 2023 at 12:52)
• Silent docstring linter (2 messages, latest: Aug 27 2023 at 20:18)
• ✔ infoview does not work in codespace (5 messages, latest: Aug 27 2023 at 15:15)
• MulHom dot notation (3 messages, latest: Aug 27 2023 at 14:37)
• allow Cache use alternative mirror URL via env (1 message, latest: Aug 27 2023 at 12:37)
• Alphabetical listing of imports (19 messages, latest: Aug 27 2023 at 12:17)
• Complete multipartite graphs (52 messages, latest: Aug 27 2023 at 11:21)
• Explicit description of condensed sets (17 messages, latest: Aug 27 2023 at 09:30)
• Turán's theorem (10 messages, latest: Aug 27 2023 at 08:28)
• Destruction and big operators (37 messages, latest: Aug 26 2023 at 23:37)
• ✔ Quiver HEq (13 messages, latest: Aug 26 2023 at 20:39)
• Patterns for binder-like notations (5 messages, latest: Aug 26 2023 at 14:56)
• shortcut for Seminorm.instMulAction? (69 messages, latest: Aug 26 2023 at 10:30)
• rw generates duplicate goals (2 messages, latest: Aug 26 2023 at 09:34)
• memory leak in tactic mode (24 messages, latest: Aug 26 2023 at 09:28)
• mathport (115 messages, latest: Aug 26 2023 at 08:56)
• Duplicates in rw? (28 messages, latest: Aug 26 2023 at 07:01)
• ∑ x ∈ s, f x instead of ∑ x in s, f x (4 messages, latest: Aug 26 2023 at 01:22)
• mathport fails (119 messages, latest: Aug 25 2023 at 20:58)
• RingCon extends (16 messages, latest: Aug 25 2023 at 18:10)
• ✔ variable in Ideal.quotientEquivAlgOfEq (4 messages, latest: Aug 25 2023 at 15:49)
• bug in ring? (52 messages, latest: Aug 25 2023 at 14:25)
• New conv => … equals tactic (14 messages, latest: Aug 25 2023 at 13:36)
• Data.Pfun naming (3 messages, latest: Aug 24 2023 at 20:28)
• cardinalities (19 messages, latest: Aug 24 2023 at 12:52)
• License choice for mathlib 4 (37 messages, latest: Aug 24 2023 at 10:04)
• Subgroup Nontrivial or ne_bot (1 message, latest: Aug 23 2023 at 23:46)
• Error: "invalid field 'countp', the environment… (4 messages, latest: Aug 23 2023 at 22:32)
• New alias syntax is coming to Mathlib! (4 messages, latest: Aug 23 2023 at 18:13)
• doc-gen ClosureOperator issue (7 messages, latest: Aug 23 2023 at 05:03)
• adding irrelevant hypotheses makes linarith succeed (6 messages, latest: Aug 23 2023 at 00:35)
• Module.Dual and linear maps (62 messages, latest: Aug 22 2023 at 12:09)
• Polynomial.map ZeroHom (7 messages, latest: Aug 22 2023 at 12:06)
• ✔ ∀ᶠ (7 messages, latest: Aug 22 2023 at 11:54)
• Stream topic (8 messages, latest: Aug 22 2023 at 11:31)
• stream events (13 messages, latest: Aug 22 2023 at 11:26)
• Finiteness of a Set (ℕ × ℕ × ℕ) with bounded components (95 messages, latest: Aug 22 2023 at 11:10)
• countp vs countP (1 message, latest: Aug 22 2023 at 08:30)
• lake exe cache get broken? (160 messages, latest: Aug 22 2023 at 00:06)
• ending of Data.Int.Cast.Defs (4 messages, latest: Aug 21 2023 at 21:24)
• cache failure whilst building CI? (3 messages, latest: Aug 21 2023 at 17:09)
• ✔ Goal is not a proposition… (21 messages, latest: Aug 20 2023 at 23:16)
• kbuzzard-quotientgroup-dewith (7 messages, latest: Aug 20 2023 at 22:32)
• Relabeling in model theory (1 message, latest: Aug 20 2023 at 21:28)
• ✔ Beginner question on ring tactic with natural integers (8 messages, latest: Aug 20 2023 at 18:06)
• refine linter (3 messages, latest: Aug 20 2023 at 12:19)
• Field.toSemifield (11 messages, latest: Aug 20 2023 at 10:31)
• #6499 broke universe polymorphism (12 messages, latest: Aug 19 2023 at 23:44)
• Universe polymorphic local instance (6 messages, latest: Aug 19 2023 at 16:14)
• tactic to apply induction on finite sets (23 messages, latest: Aug 19 2023 at 00:10)
• doc-gen print global doc-string first (16 messages, latest: Aug 18 2023 at 20:44)
• mathlib-preferred calc style (14 messages, latest: Aug 18 2023 at 19:21)
• Integral and Expectation (11 messages, latest: Aug 18 2023 at 14:13)
• bump to nightly-2023-08-17 (16 messages, latest: Aug 18 2023 at 07:59)
• "library scale" testing of tactics (15 messages, latest: Aug 18 2023 at 07:11)
• exact? crashes (15 messages, latest: Aug 17 2023 at 21:40)
• default instance ignored in intro (1 message, latest: Aug 17 2023 at 16:12)
• SSL for speed.lean-fro.org (4 messages, latest: Aug 17 2023 at 16:11)
• Issues in !4#2123 (Topology.CompactOpen) (35 messages, latest: Aug 17 2023 at 11:50)
• Meaning of numbers when one builds mathlib (7 messages, latest: Aug 16 2023 at 23:03)
• Obj component in Cat (5 messages, latest: Aug 16 2023 at 22:55)
• LinearMap.proj (3 messages, latest: Aug 16 2023 at 22:23)
• simpNF failure in unrelated file (6 messages, latest: Aug 16 2023 at 19:47)
• rcases modifies assumptions (15 messages, latest: Aug 16 2023 at 11:01)
• protected (20 messages, latest: Aug 16 2023 at 10:29)
• extensionality for functors (39 messages, latest: Aug 15 2023 at 22:19)
• Instance priorities for quotients of MvPolynomial (27 messages, latest: Aug 15 2023 at 14:21)
• have EquivLike using FunLike? (3 messages, latest: Aug 15 2023 at 11:59)
• Cache build between branch switches (5 messages, latest: Aug 14 2023 at 19:22)
• Log.Base and Zmod.Basic conflicting with each other (?) (10 messages, latest: Aug 13 2023 at 22:32)
• Why does nlinarith succeed? (6 messages, latest: Aug 13 2023 at 22:30)
• Flypitch integration (17 messages, latest: Aug 13 2023 at 22:09)
• count_heartbeat says... (11 messages, latest: Aug 13 2023 at 20:36)
• with in definitions (11 messages, latest: Aug 13 2023 at 19:58)
• Finishing a review as a non-maintainer? (4 messages, latest: Aug 13 2023 at 08:17)
• CategoryTheory.Category.mk (6 messages, latest: Aug 13 2023 at 03:57)
• Equiv.cast for structures (16 messages, latest: Aug 11 2023 at 21:19)
• progress on fail_if_no_progress (20 messages, latest: Aug 11 2023 at 11:38)
• tryThese? (8 messages, latest: Aug 11 2023 at 00:16)
• EReal instance (18 messages, latest: Aug 10 2023 at 21:29)
• calc mode for types (13 messages, latest: Aug 10 2023 at 20:45)
• => notation (152 messages, latest: Aug 10 2023 at 13:22)
• std fails to build after lake update (36 messages, latest: Aug 10 2023 at 11:59)
• cannot find synthesization order for instance (3 messages, latest: Aug 10 2023 at 04:35)
• 100 theorems list and undergrad targets (61 messages, latest: Aug 09 2023 at 21:55)
• ✔ Foo.baz_of_bar (7 messages, latest: Aug 09 2023 at 13:29)
• lake exe cache get offline (7 messages, latest: Aug 09 2023 at 11:48)
• initial imports (11 messages, latest: Aug 08 2023 at 18:41)
• divX vs divByMonic X (13 messages, latest: Aug 08 2023 at 14:58)
• Mathlib causes failure in mutual recursive definition (74 messages, latest: Aug 08 2023 at 05:08)
• commit messages (2 messages, latest: Aug 08 2023 at 04:37)
• same level as (13 messages, latest: Aug 08 2023 at 00:47)
• universe level in SimplyConnectedSpace.ofConnected (2 messages, latest: Aug 07 2023 at 20:30)
• Algebra.TensorProduct.rid as isomorphism over the larger … (31 messages, latest: Aug 07 2023 at 18:41)
• suffices syntax (18 messages, latest: Aug 07 2023 at 18:20)
• leantar too old (lean exe cache get not working) (96 messages, latest: Aug 07 2023 at 16:40)
• AlgEquiv.toFun_eq_coe (7 messages, latest: Aug 07 2023 at 12:45)
• meta code reviewers (10 messages, latest: Aug 07 2023 at 11:47)
• Quotient slowdowns (41 messages, latest: Aug 07 2023 at 11:46)
• leangz error (6 messages, latest: Aug 07 2023 at 08:35)
• panic with rw? (3 messages, latest: Aug 07 2023 at 00:23)
• Missing library notes (5 messages, latest: Aug 06 2023 at 23:14)
• doc-gen4 (11 messages, latest: Aug 06 2023 at 23:12)
• rfl vs by rfl in instance diamonds (10 messages, latest: Aug 06 2023 at 14:59)
• Where can I get the velcom benchmark script? (3 messages, latest: Aug 06 2023 at 00:56)
• Why did the community decide to use "special values"? (19 messages, latest: Aug 06 2023 at 00:37)
• Bug for quotients? (5 messages, latest: Aug 05 2023 at 16:33)
• extract_goal: universe bug? (10 messages, latest: Aug 05 2023 at 12:52)
• MetaM and Option (5 messages, latest: Aug 04 2023 at 13:03)
• is there an existing NTT proof? (4 messages, latest: Aug 04 2023 at 03:50)
• Universe issue (infinite loop) (32 messages, latest: Aug 03 2023 at 21:41)
• Matroids in mathlib - feedback? (27 messages, latest: Aug 03 2023 at 18:52)
• isBlacklisted (1 message, latest: Aug 03 2023 at 14:40)
• naming (2 messages, latest: Aug 03 2023 at 05:40)
• ✔ field_simp and positivity (9 messages, latest: Aug 02 2023 at 22:36)
• bad instance for ordered add comm monoids? (10 messages, latest: Aug 02 2023 at 16:26)
• Working with Multivariate Polynomials (13 messages, latest: Aug 01 2023 at 18:34)
• Fixing docstrings in Mathlib 4 (16 messages, latest: Aug 01 2023 at 08:15)
• duplicate instances in docs? (3 messages, latest: Jul 31 2023 at 20:52)
• Slow TC for Module (10 messages, latest: Jul 31 2023 at 18:31)
• macos sonoma (63 messages, latest: Jul 31 2023 at 14:36)
• alias command ordering (11 messages, latest: Jul 31 2023 at 13:57)
• Contribute to Mathlib4 (2 messages, latest: Jul 30 2023 at 07:46)
• ✔ lean4/mathlib4 import issue on Gentoo (26 messages, latest: Jul 29 2023 at 18:19)
• import Mathlib failed in lake new created local project (2 messages, latest: Jul 29 2023 at 16:21)
• Define RHS in conv mode (20 messages, latest: Jul 29 2023 at 08:26)
• LaTeX in Lean? (38 messages, latest: Jul 29 2023 at 02:44)
• removing unprimed closure induction principles (15 messages, latest: Jul 28 2023 at 18:20)
• Typeclass search for mem notation (10 messages, latest: Jul 28 2023 at 12:35)
• documentation TODOs (8 messages, latest: Jul 28 2023 at 03:00)
• ← lifting over if footgun (14 messages, latest: Jul 28 2023 at 02:18)
• bump to 2023-07-15 (15 messages, latest: Jul 28 2023 at 01:55)
• order of element is the cardinality of its closure (4 messages, latest: Jul 28 2023 at 00:11)
• Linter idea: h1 h2 hypotheses in induction (4 messages, latest: Jul 26 2023 at 21:47)
• port progress (5094 messages, latest: Jul 26 2023 at 18:10)
• Error: unreachable @ extractMainModule (1 message, latest: Jul 26 2023 at 17:50)
• LinearMap.CompatibleSMul (7 messages, latest: Jul 26 2023 at 12:29)
• invalid pattern, constructor or constant marked with '[match (6 messages, latest: Jul 26 2023 at 12:07)
• Failed to synthesize DecidablePred (5 messages, latest: Jul 25 2023 at 20:57)
• removing after-port? (7 messages, latest: Jul 25 2023 at 06:53)
• Newton's identities (1 message, latest: Jul 24 2023 at 18:57)
• let's not crank maxHeartbeats as low as possible (22 messages, latest: Jul 24 2023 at 11:04)
• Trace simp (5 messages, latest: Jul 24 2023 at 09:29)
• Transitive closure in instance search (3 messages, latest: Jul 24 2023 at 04:56)
• ext for DFinsupp.ext (22 messages, latest: Jul 24 2023 at 01:34)
• ✔ Help with mathlib docs (8 messages, latest: Jul 23 2023 at 17:42)
• Set as a structure (1 message, latest: Jul 23 2023 at 14:04)
• Simp priority (16 messages, latest: Jul 23 2023 at 08:22)
• changing algebra instance priorities (54 messages, latest: Jul 22 2023 at 21:13)
• Mathlib is open for refactoring! (5 messages, latest: Jul 22 2023 at 13:27)
• aligns for refactored content (5 messages, latest: Jul 22 2023 at 08:06)
• convert (3 messages, latest: Jul 21 2023 at 21:09)
• Bug in fin_cases? (6 messages, latest: Jul 21 2023 at 18:37)
• RePred (63 messages, latest: Jul 21 2023 at 11:03)
• library_search fails to find theorem (14 messages, latest: Jul 21 2023 at 01:02)
• cancel_denoms field_simp and casts (31 messages, latest: Jul 20 2023 at 19:03)
• notation capturing type information (27 messages, latest: Jul 20 2023 at 18:21)
• CoeOut instance from Submodule R M to ModuleCat R (9 messages, latest: Jul 20 2023 at 16:40)
• instance breaking FunLike (6 messages, latest: Jul 20 2023 at 15:46)
• Getting a dictionary of aligns in a json file (3 messages, latest: Jul 20 2023 at 13:57)
• putting mathlib3 in the git history (58 messages, latest: Jul 20 2023 at 12:55)
• comment highlighting in Algebra.HierarchyDesign (10 messages, latest: Jul 20 2023 at 08:18)
• CI stuck on Add annotations (5 messages, latest: Jul 20 2023 at 02:36)
• Running javascript in the infoview with ProofWidgets (9 messages, latest: Jul 20 2023 at 00:24)
• Change of the proof of WellFounded causes timeouts (4 messages, latest: Jul 19 2023 at 22:26)
• #align_import (76 messages, latest: Jul 19 2023 at 20:47)
• Type Class question (6 messages, latest: Jul 19 2023 at 19:41)
• ✔ rcases got stronger? (7 messages, latest: Jul 19 2023 at 19:29)
• Natural map from Fin n -> Bool to Fin(2^n) (15 messages, latest: Jul 19 2023 at 15:08)
• panic with SimpleGraph fun (17 messages, latest: Jul 19 2023 at 13:26)
• detect if we are running in CI (4 messages, latest: Jul 19 2023 at 01:29)
• How to make InferInstance ignore my new instance (39 messages, latest: Jul 19 2023 at 00:31)
• ZMod.coe_add_eq_ite changed (5 messages, latest: Jul 18 2023 at 16:15)
• #outofsync (9 messages, latest: Jul 18 2023 at 02:27)
• leantar cache (18 messages, latest: Jul 18 2023 at 00:45)
• pushed to master (8 messages, latest: Jul 17 2023 at 18:36)
• "(kernel) declaration has metavariables" (54 messages, latest: Jul 17 2023 at 18:29)
• non-aligned definitions (51 messages, latest: Jul 17 2023 at 17:05)
• Improve error message of tauto (10 messages, latest: Jul 17 2023 at 11:56)
• std4 / Lean4 bump (32 messages, latest: Jul 17 2023 at 10:45)
• source for open (2 messages, latest: Jul 17 2023 at 08:12)
• t-* labels on github (8 messages, latest: Jul 17 2023 at 04:57)
• ✔ ℕ vs Nat (12 messages, latest: Jul 17 2023 at 01:21)
• new project setup fails (7 messages, latest: Jul 16 2023 at 22:38)
• norm_cast leaks Int.subSubNat (4 messages, latest: Jul 16 2023 at 19:39)
• Porting files from core (5 messages, latest: Jul 16 2023 at 18:17)
• int.coe_nat_inj (16 messages, latest: Jul 16 2023 at 17:53)
• psigma.lex_wf (10 messages, latest: Jul 16 2023 at 16:45)
• Data.Rat.MetaDefs (12 messages, latest: Jul 16 2023 at 16:23)
• mathport/Oneshot (2 messages, latest: Jul 16 2023 at 09:33)
• #5571 (24 messages, latest: Jul 16 2023 at 00:17)
• OfNat.ofNat visible (29 messages, latest: Jul 15 2023 at 20:42)
• non-terminal simps (2 messages, latest: Jul 15 2023 at 18:15)
• port benchmark (446 messages, latest: Jul 15 2023 at 13:45)
• Making SDiff heterogeneous? (39 messages, latest: Jul 15 2023 at 13:10)
• mathlib3 is frozen (1 message, latest: Jul 15 2023 at 12:03)
• #5663 (58 messages, latest: Jul 15 2023 at 08:35)
• How do I define decidableLE for simple quotient type. (16 messages, latest: Jul 14 2023 at 20:12)
• MonadExcept in the ContT monad (6 messages, latest: Jul 14 2023 at 18:29)
• Fin in std4 (4 messages, latest: Jul 14 2023 at 13:13)
• BigProd permutations - implementation h. (10 messages, latest: Jul 14 2023 at 11:14)
• Mario's FMM 2021 talk (47 messages, latest: Jul 14 2023 at 08:19)
• A problem with lean (10 messages, latest: Jul 14 2023 at 08:08)
• String.isSuffixOf (3 messages, latest: Jul 13 2023 at 23:57)
• Qq with mkFreshLevelMVar (5 messages, latest: Jul 13 2023 at 17:20)
• bit0 deprecated (63 messages, latest: Jul 13 2023 at 17:09)
• ContMdiffMfderiv (29 messages, latest: Jul 12 2023 at 22:23)
• what_changed? tactic (6 messages, latest: Jul 12 2023 at 17:18)
• Warning: some files were not found in the cache. (20 messages, latest: Jul 12 2023 at 06:38)
• slim_check instantiating mvars missing? (3 messages, latest: Jul 11 2023 at 22:19)
• porting .array files whose PR's were closed? (50 messages, latest: Jul 11 2023 at 18:37)
• solve_by_elim going in circles (4 messages, latest: Jul 11 2023 at 18:28)
• Metamathematics: Theorems by Domain Areas (40 messages, latest: Jul 11 2023 at 04:01)
• Id vs id as a monad (8 messages, latest: Jul 10 2023 at 20:44)
• port-status#data/buffer/parser (11 messages, latest: Jul 10 2023 at 17:23)
• Data.Fintype.Array (11 messages, latest: Jul 10 2023 at 10:12)
• crazy coercion (39 messages, latest: Jul 10 2023 at 10:00)
• wrong type of dot (7 messages, latest: Jul 09 2023 at 21:45)
• Nat.repeat vs Nat.iterate (7 messages, latest: Jul 09 2023 at 16:51)
• #stalled PRs (55 messages, latest: Jul 09 2023 at 11:02)
• introducing docstrings while porting (16 messages, latest: Jul 09 2023 at 00:16)
• #5600 CliffordAlgebra.EvenEquiv (6 messages, latest: Jul 08 2023 at 20:34)
• port dashboard (6 messages, latest: Jul 08 2023 at 10:18)
• ✔ Geometry.Manifold.Algebra.LeftInvariantDerivation #5665 (7 messages, latest: Jul 08 2023 at 05:11)
• ✔ x+y≤z → x≤z (10 messages, latest: Jul 08 2023 at 01:33)
• #5094 status (3 messages, latest: Jul 07 2023 at 20:22)
• ModelTheory.Fraisse #4565 (17 messages, latest: Jul 07 2023 at 18:27)
• Notation for dilation (2 messages, latest: Jul 07 2023 at 13:07)
• scope of local notations (3 messages, latest: Jul 07 2023 at 11:14)
• forward-port 19105 #5749 (2 messages, latest: Jul 07 2023 at 10:58)
• Traversable deriving handlers #5606 (1 message, latest: Jul 07 2023 at 10:55)
• #5750 abstract continuous functional calculus (4 messages, latest: Jul 07 2023 at 08:37)
• !4#5088 CategoryTheory.Monad.Monadicity (14 messages, latest: Jul 07 2023 at 07:32)
• Algebra.Category.Algebra.Limits #5716 (8 messages, latest: Jul 07 2023 at 06:57)
• CategoryTheory.Monad.Monadicity #5088 (1 message, latest: Jul 07 2023 at 04:32)
• Universe inequalities (28 messages, latest: Jul 06 2023 at 23:37)
• #4335 upper half plane basic (19 messages, latest: Jul 06 2023 at 18:52)
• Fin as a coercion? (4 messages, latest: Jul 06 2023 at 18:23)
• ✔ Refactor (vector) bundles now? (25 messages, latest: Jul 06 2023 at 15:07)
• Archive.Examples.MersennePrimes #5704 (59 messages, latest: Jul 06 2023 at 14:44)
• Autogenerate "forall" and "exists" lemmas (12 messages, latest: Jul 06 2023 at 01:17)
• #4635 GromovHausdorff (14 messages, latest: Jul 05 2023 at 14:08)
• #5727 smooth bundle hom (1 message, latest: Jul 05 2023 at 07:12)
• Algebra.Category.Algebra.Basic #4504 (6 messages, latest: Jul 05 2023 at 04:53)
• loop space notation (6 messages, latest: Jul 04 2023 at 17:36)
• ZMod maximum recursion depth (5 messages, latest: Jul 04 2023 at 15:07)
• OfNat for Units? (3 messages, latest: Jul 04 2023 at 14:28)
• Instances in refine (for port/RingTheory.Jacobson) (5 messages, latest: Jul 04 2023 at 07:30)
• #4338 Jacobson (12 messages, latest: Jul 03 2023 at 20:12)
• ModuleCat.isModule not defeq (23 messages, latest: Jul 03 2023 at 16:38)
• Boundaryless models (14 messages, latest: Jul 03 2023 at 15:30)
• simp attrs (5 messages, latest: Jul 03 2023 at 05:14)
• Reintroducing quotient rings in RingTheory.Polynomial.Basic (5 messages, latest: Jul 02 2023 at 19:04)
• nsmul/zsmul fields (5 messages, latest: Jul 02 2023 at 17:48)
• Possible future name collision (42 messages, latest: Jul 02 2023 at 17:04)
• Notation precedence: compl (30 messages, latest: Jul 02 2023 at 09:46)
• ✔ product of fins (16 messages, latest: Jul 01 2023 at 18:45)
• meta code needed for restrict_tac/sheaf_restrict (1 message, latest: Jul 01 2023 at 09:50)
• mathport recompiles mathlib (6 messages, latest: Jul 01 2023 at 02:06)
• package for mathport? (13 messages, latest: Jun 30 2023 at 21:49)
• pp_extended_field_notation (9 messages, latest: Jun 30 2023 at 18:15)
• roadmap/ (3 messages, latest: Jun 29 2023 at 23:38)
• apply? cache corrupts when updating mathlib (8 messages, latest: Jun 29 2023 at 10:34)
• !4#5519 - Algebra.Category.FGModuleCat.Limits (7 messages, latest: Jun 29 2023 at 07:54)
• weird tactic bug (15 messages, latest: Jun 29 2023 at 06:26)
• panic and error with rw? (14 messages, latest: Jun 29 2023 at 01:23)
• rw seeing through type synonym? (55 messages, latest: Jun 28 2023 at 23:33)
• aesop (35 messages, latest: Jun 28 2023 at 20:24)
• ag in ml4 (24 messages, latest: Jun 28 2023 at 14:52)
• split_ifs boxes itself into a corner (10 messages, latest: Jun 28 2023 at 10:15)
• ✔ mathport and moving theorems (3 messages, latest: Jun 28 2023 at 10:00)
• ✔ mathport lemma (3 messages, latest: Jun 28 2023 at 08:37)
• !4#3463 universe constraint issues (229 messages, latest: Jun 28 2023 at 05:00)
• WittVector saga (44 messages, latest: Jun 27 2023 at 19:38)
• ∀ x > 0 (7 messages, latest: Jun 27 2023 at 17:46)
• Changelog of non-BC changes? (20 messages, latest: Jun 27 2023 at 13:38)
• #4951 CategoryTheory.Closed.Ideal (8 messages, latest: Jun 27 2023 at 08:40)
• check_instances (3 messages, latest: Jun 27 2023 at 05:43)
• iff lemmas for equivs (4 messages, latest: Jun 27 2023 at 05:24)
• import graph (6 messages, latest: Jun 27 2023 at 03:13)
• ✔ semiOutParam for SMulMemClass? (3 messages, latest: Jun 27 2023 at 00:41)
• Different Instance on same structure (10 messages, latest: Jun 26 2023 at 22:06)
• #5480 SetTheory.Game.Ordinal (13 messages, latest: Jun 26 2023 at 21:56)
• Notation error for norm (10 messages, latest: Jun 26 2023 at 21:24)
• additivized IsConj (6 messages, latest: Jun 26 2023 at 17:15)
• equivalent of leanprojet get-cache (14 messages, latest: Jun 26 2023 at 15:31)
• Liminf/Limsup naming (4 messages, latest: Jun 26 2023 at 14:33)
• does doc-gen4 support zulip-style linkifiers? (1 message, latest: Jun 26 2023 at 08:34)
• porting "unneeded" files (5 messages, latest: Jun 26 2023 at 06:18)
• defeq for the tangent space (13 messages, latest: Jun 25 2023 at 21:29)
• positivity (6 messages, latest: Jun 25 2023 at 18:20)
• congr% term elaborator (11 messages, latest: Jun 25 2023 at 17:20)
• !4#4777 NumberTheory.Bertrand (1 message, latest: Jun 25 2023 at 15:41)
• docs4 not updated (65 messages, latest: Jun 25 2023 at 14:13)
• Porting local tactics (9 messages, latest: Jun 24 2023 at 17:54)
• !4#5424 FieldTheory.AbelRuffini (5 messages, latest: Jun 24 2023 at 09:40)
• 1 error left in !4#5397 AddCharacter (5 messages, latest: Jun 24 2023 at 05:55)
• coercion issue in NumberTheory.LegendreSymbol.MulCharacter (22 messages, latest: Jun 23 2023 at 20:30)
• simps for MulOpposite (7 messages, latest: Jun 23 2023 at 20:08)
• Timeout in set .. with (20 messages, latest: Jun 23 2023 at 18:00)
• Declarations generated by simps (2 messages, latest: Jun 23 2023 at 15:17)
• simp normal form for Vector indexing: get vs .\[.\] (34 messages, latest: Jun 23 2023 at 15:09)
• #4791 ValuationSubring (9 messages, latest: Jun 23 2023 at 12:41)
• mysterious finsupp related timeout (104 messages, latest: Jun 23 2023 at 10:02)
• simp for ModelProd (8 messages, latest: Jun 23 2023 at 03:22)
• upper half plane topology (46 messages, latest: Jun 22 2023 at 23:27)
• abel bug? (4 messages, latest: Jun 22 2023 at 22:43)
• obliterating conjInvariantSubalgebra (3 messages, latest: Jun 22 2023 at 20:39)
• !4#5366 (7 messages, latest: Jun 22 2023 at 11:01)
• Analysis.SpecialFunctions.Gaussian (2 messages, latest: Jun 22 2023 at 06:38)
• wlog … replacing …? (10 messages, latest: Jun 22 2023 at 05:10)
• lean 4 macro + loop (7 messages, latest: Jun 22 2023 at 04:08)
• wlog error (9 messages, latest: Jun 22 2023 at 03:00)
• !4#5294 help wanted (2 messages, latest: Jun 22 2023 at 00:46)
• Bug with tfae_have? (12 messages, latest: Jun 21 2023 at 23:28)
• Cases does not change assumptions (2 messages, latest: Jun 21 2023 at 22:27)
• dec_trivial with metavariables (10 messages, latest: Jun 21 2023 at 21:28)
• #5335 NumberTheory.Cyclotomic.Basic (1 message, latest: Jun 21 2023 at 15:43)
• !4#5159 FieldTheory.PolynomialGaloisGroup (17 messages, latest: Jun 21 2023 at 11:43)
• Lean doc preview (1 message, latest: Jun 21 2023 at 02:24)
• ✔ Porting Algebra.Category.GroupCat.Adjunctions (9 messages, latest: Jun 21 2023 at 01:48)
• Running tests with options (11 messages, latest: Jun 21 2023 at 01:47)
• on-click have? using h (11 messages, latest: Jun 20 2023 at 22:07)
• Porting Analysis.Fourier.PoissonSummation (20 messages, latest: Jun 20 2023 at 19:06)
• Le.le simp_arith Int issue (12 messages, latest: Jun 20 2023 at 16:50)
• bad apply? suggestion (1 message, latest: Jun 20 2023 at 16:32)
• Auto-implicits (39 messages, latest: Jun 20 2023 at 14:32)
• !4#5199: timeout problem in birthday problem (12 messages, latest: Jun 20 2023 at 09:23)
• !4#5256 RingTheory.Trace (57 messages, latest: Jun 20 2023 at 09:22)
• No goals (4 messages, latest: Jun 20 2023 at 07:28)
• timeouts (17 messages, latest: Jun 20 2023 at 07:27)
• Factorial notation parse error (12 messages, latest: Jun 19 2023 at 17:02)
• !4#5249 NumberTheory.KummerDedekind (7 messages, latest: Jun 19 2023 at 16:57)
• Slow coercions (11 messages, latest: Jun 19 2023 at 14:11)
• Error "unknown package 'analysis'" (6 messages, latest: Jun 19 2023 at 13:32)
• !4#4490 Analysis.Matrix (5 messages, latest: Jun 19 2023 at 12:05)
• ✔ ring_nf regression? (6 messages, latest: Jun 19 2023 at 06:07)
• bug in borelize (5 messages, latest: Jun 19 2023 at 01:26)
• !4#5074 FieldTheory.IsAlgClosed.AlgebraicClosure (14 messages, latest: Jun 18 2023 at 20:36)
• !4#4891 FieldTheory.SplittingField (348 messages, latest: Jun 18 2023 at 12:57)
• power-up for ext (41 messages, latest: Jun 18 2023 at 12:48)
• [Fact] in def (17 messages, latest: Jun 17 2023 at 19:47)
• port ConditionalExpectation.Basic !4#4898 (3 messages, latest: Jun 17 2023 at 12:25)
• apply bug with fun a => _ (4 messages, latest: Jun 17 2023 at 02:06)
• mathport on a branch (4 messages, latest: Jun 17 2023 at 01:27)
• deriving not working (4 messages, latest: Jun 17 2023 at 00:09)
• ac_refl (9 messages, latest: Jun 16 2023 at 23:37)
• problems with lake exe cache (56 messages, latest: Jun 16 2023 at 11:37)
• push_neg behavior (31 messages, latest: Jun 16 2023 at 05:20)
• Archive.100-theorems-list.XXTheoremName causes error !4#5114 (7 messages, latest: Jun 16 2023 at 04:23)
• Missing simp for adjoin (15 messages, latest: Jun 16 2023 at 03:54)
• Measure is overloaded (8 messages, latest: Jun 15 2023 at 20:44)
• DecidableLE for Finset (15 messages, latest: Jun 15 2023 at 15:33)
• !4#5071 FieldTheory.PrimitiveElement (5 messages, latest: Jun 15 2023 at 11:16)
• library_search crashes in the web editor (4 messages, latest: Jun 15 2023 at 10:09)
• simp lemmas with side conditions (23 messages, latest: Jun 15 2023 at 02:41)
• Renaming library_search (36 messages, latest: Jun 15 2023 at 00:43)
• Eigenvalue coercion (9 messages, latest: Jun 14 2023 at 20:12)
• AlgebraicGeometry.OpenImmersion.Basic (22 messages, latest: Jun 14 2023 at 17:07)
• Tactic (2 messages, latest: Jun 14 2023 at 12:21)
• Proving Interval Integrability (4 messages, latest: Jun 14 2023 at 09:56)
• Analysis.Analytic.Composition !4#4572 (12 messages, latest: Jun 14 2023 at 05:37)
• Porting Dlist.lean (16 messages, latest: Jun 14 2023 at 01:58)
• Concrete cycle notation (6 messages, latest: Jun 14 2023 at 01:38)
• !4#5022, forward port of #19179 (6 messages, latest: Jun 14 2023 at 00:18)
• triage of "Porting notes" (39 messages, latest: Jun 13 2023 at 19:53)
• !4#4852 heartbeats of the linter (9 messages, latest: Jun 13 2023 at 19:25)
• TensorProduct.curry (12 messages, latest: Jun 13 2023 at 06:46)
• Can Vector.map_cons be simp (7 messages, latest: Jun 12 2023 at 15:08)
• unrelated build failure in !4#4831 (7 messages, latest: Jun 12 2023 at 13:21)
• Wrong universes (21 messages, latest: Jun 12 2023 at 12:57)
• FunLike issues (74 messages, latest: Jun 11 2023 at 15:45)
• !4#4949 Algebra.Category.Module.FilteredColimits (17 messages, latest: Jun 11 2023 at 12:00)
• group cohomology mathlib3 PR (6 messages, latest: Jun 11 2023 at 07:12)
• op_norm tactic (5 messages, latest: Jun 11 2023 at 02:13)
• superscript parser (37 messages, latest: Jun 10 2023 at 21:36)
• !4#4629 Cannot find synthesization order (1 message, latest: Jun 10 2023 at 09:07)
• simp regression (28 messages, latest: Jun 10 2023 at 02:32)
• !4#4352 apply_congr in BernoulliPolynomials (2 messages, latest: Jun 09 2023 at 16:56)
• !4#4888 IsAlgClosed (4 messages, latest: Jun 09 2023 at 15:35)
• !4#4890 FieldTheory.Fixed (1 message, latest: Jun 09 2023 at 13:13)
• !4#4856 FieldTheory.Normal (20 messages, latest: Jun 09 2023 at 05:41)
• #19094 and !4#4656 (3 messages, latest: Jun 09 2023 at 02:33)
• Mathport oneshot (153 messages, latest: Jun 08 2023 at 23:26)
• deprecation warning from ProofWidgets (3 messages, latest: Jun 08 2023 at 17:15)
• simpNF linter timeout !4#4852 (1 message, latest: Jun 08 2023 at 15:52)
• !4#4857 Magma.ofHom (3 messages, latest: Jun 08 2023 at 15:14)
• GroupTheory.FreeGroup mathlib4#1867 (29 messages, latest: Jun 08 2023 at 09:13)
• Lean 4 adds variable to args for no reason (24 messages, latest: Jun 08 2023 at 02:37)
• RingTheory.Adjoin.Field is slow (27 messages, latest: Jun 07 2023 at 22:00)
• Data.Vector3 (16 messages, latest: Jun 07 2023 at 21:01)
• Local notation priority (6 messages, latest: Jun 07 2023 at 19:46)
• bors crashed (60 messages, latest: Jun 07 2023 at 18:14)
• CI (4 messages, latest: Jun 07 2023 at 17:53)
• setting up Gitpod (14 messages, latest: Jun 07 2023 at 16:44)
• local instance cannot find synthesization order in porting (22 messages, latest: Jun 07 2023 at 16:29)
• porting dashboard (19 messages, latest: Jun 07 2023 at 14:38)
• !4#4688 WittVector.Basic (5 messages, latest: Jun 07 2023 at 14:36)
• !4#4761 universe issues (6 messages, latest: Jun 07 2023 at 12:12)
• cleaning up the to-be-ported list (12 messages, latest: Jun 07 2023 at 09:42)
• !4#3836 CategoryTheory.Sites.CompatiblePlus (14 messages, latest: Jun 07 2023 at 04:41)
• !4#4710 IntervalIntegral (8 messages, latest: Jun 07 2023 at 03:14)
• tactic combinator to require that a tactic changes the goal? (3 messages, latest: Jun 07 2023 at 00:55)
• no space left on device (52 messages, latest: Jun 06 2023 at 23:15)
• Golfing a have in !4#4738 (15 messages, latest: Jun 06 2023 at 17:25)
• !4#4677 RootsOfUnity.Basic (4 messages, latest: Jun 06 2023 at 13:52)
• mathport: big operators (47 messages, latest: Jun 06 2023 at 05:19)
• Lean 4 doesn't add lemma to the environment (6 messages, latest: Jun 06 2023 at 03:47)
• trans/symm changes (1 message, latest: Jun 05 2023 at 22:38)
• ambiguous identifier (5 messages, latest: Jun 05 2023 at 14:49)
• Trimming dependencies on SplittingField (54 messages, latest: Jun 05 2023 at 09:26)
• Fintype (Group G) (20 messages, latest: Jun 05 2023 at 09:07)
• Attribute pp_nodot (9 messages, latest: Jun 05 2023 at 06:55)
• coe conflict in concrete categories (17 messages, latest: Jun 05 2023 at 06:06)
• Expr.foldlM (4 messages, latest: Jun 05 2023 at 05:19)
• AdjoinRoot: gigantic terms take VS Code down (12 messages, latest: Jun 05 2023 at 00:35)
• New Project that uses MathLib4 (128 messages, latest: Jun 04 2023 at 23:29)
• polyrith and "try this" (2 messages, latest: Jun 04 2023 at 17:11)
• path to calculus (4 messages, latest: Jun 04 2023 at 13:40)
• notation3 in docs (1 message, latest: Jun 03 2023 at 19:32)
• Operator norm (35 messages, latest: Jun 03 2023 at 19:07)
• Miraculous rw in Lean 3 (9 messages, latest: Jun 03 2023 at 16:53)
• mathlib4 permission (4 messages, latest: Jun 02 2023 at 17:11)
• MeasureTheory.Measure.Lebesgue.Basic !4#4552 (11 messages, latest: Jun 02 2023 at 16:09)
• start_port.sh fails (124 messages, latest: Jun 02 2023 at 14:27)
• !4#4557 Probability.Indepence.Basic (7 messages, latest: Jun 02 2023 at 13:12)
• missing ppSpace for mathport? (12 messages, latest: Jun 02 2023 at 05:38)
• about fderiv and the transformation of the types (1 message, latest: Jun 02 2023 at 02:09)
• splitting field discussion @ porting meeting (46 messages, latest: Jun 02 2023 at 00:34)
• !4#4465 lp (13 messages, latest: Jun 01 2023 at 18:17)
• simps config (10 messages, latest: Jun 01 2023 at 12:40)
• multiple files (100 messages, latest: Jun 01 2023 at 11:38)
• min/max definitions non-alignment (41 messages, latest: Jun 01 2023 at 10:57)
• Shadow notation (8 messages, latest: Jun 01 2023 at 08:21)
• autolinking files in docs (8 messages, latest: Jun 01 2023 at 07:54)
• dsimp in instances (11 messages, latest: Jun 01 2023 at 05:47)
• help wanted porting Analysis.Calculus.ContDiffDef !4#4256 (3 messages, latest: Jun 01 2023 at 02:49)
• library_search failing to apply symm (8 messages, latest: Jun 01 2023 at 02:04)
• Broken line breaking in mathport output (1 message, latest: May 31 2023 at 08:58)
• "elab_inline" instead of notation? (6 messages, latest: May 31 2023 at 08:25)
• Option for deactivating autoparams (5 messages, latest: May 31 2023 at 01:04)
• simpNF bug? (4 messages, latest: May 30 2023 at 22:33)
• linarith (23 messages, latest: May 30 2023 at 17:47)
• !4#4085 (36 messages, latest: May 30 2023 at 16:53)
• SemilatSup coercion (25 messages, latest: May 30 2023 at 12:06)
• lean-graded-rings-supersymmetry (1 message, latest: May 30 2023 at 02:28)
• Strange push_neg behaviour (17 messages, latest: May 29 2023 at 20:49)
• !4#4473 Proving that Gram–Schmidt terminates (19 messages, latest: May 29 2023 at 20:00)
• liftHom or LiftHom? (30 messages, latest: May 29 2023 at 15:28)
• leanproject –port-complete (174 messages, latest: May 29 2023 at 08:07)
• waits requested (14 messages, latest: May 28 2023 at 17:43)
• archive (8 messages, latest: May 28 2023 at 17:32)
• ring and succ (12 messages, latest: May 28 2023 at 16:38)
• Inductive type port maybe needs to add the type parameter (8 messages, latest: May 28 2023 at 06:01)
• #align statement RHS (6 messages, latest: May 28 2023 at 01:04)
• Lean 4 survival guide for Lean 3 users (16 messages, latest: May 27 2023 at 19:01)
• mathport on external projects (9 messages, latest: May 27 2023 at 18:53)
• Is @[protect_proj] obsolete? (11 messages, latest: May 27 2023 at 17:34)
• filter_upwards missing an instantiateMVars? (9 messages, latest: May 27 2023 at 16:32)
• docs4#TopologicalSpace.Opens.leSupr (2 messages, latest: May 27 2023 at 15:04)
• algebra.category.Module.algebra (14 messages, latest: May 27 2023 at 13:48)
• ✔ include V in Inversion.lean (28 messages, latest: May 27 2023 at 11:57)
• Question about FinEnum (10 messages, latest: May 26 2023 at 20:30)
• !4#4322 last dependency for Ext (9 messages, latest: May 26 2023 at 16:26)
• !4#4345 Analysis.NormedSpace.PiLp (4 messages, latest: May 26 2023 at 14:46)
• !#4335 Analysis.Complex.UpperHalfPlane.Basic (5 messages, latest: May 26 2023 at 12:47)
• !4#4344 NumberTheory.Padics.Hensel (8 messages, latest: May 26 2023 at 12:25)
• auto-fix comments (12 messages, latest: May 25 2023 at 21:36)
• looping in simp set (2 messages, latest: May 25 2023 at 18:14)
• norm_cast: badly shaped lemma (35 messages, latest: May 25 2023 at 15:48)
• ✔ !4#4271 RingTheory.AdjoinRoot (31 messages, latest: May 25 2023 at 15:08)
• ✔ Mathlib porting status doesn't show the dependency graph (5 messages, latest: May 25 2023 at 07:45)
• FOL logic with unary predicates (74 messages, latest: May 25 2023 at 06:22)
• subsingleton simp failure in presence of instance (7 messages, latest: May 25 2023 at 01:21)
• @\[ext\] is too eager (4 messages, latest: May 25 2023 at 00:13)
• calc and isBigO (7 messages, latest: May 24 2023 at 23:44)
• !4#4200 (21 messages, latest: May 24 2023 at 19:39)
• !4#4280 Analysis.InnerProductSpace.Basic (11 messages, latest: May 24 2023 at 18:56)
• [anonymous] (4 messages, latest: May 24 2023 at 15:41)
• mathlib3port 404 (7 messages, latest: May 24 2023 at 11:59)
• lake exe cache get fails when username contains spaces (3 messages, latest: May 24 2023 at 09:03)
• porting the prelude (3 messages, latest: May 24 2023 at 05:54)
• !4#4052 Algebra.DirectLimit (needed for Ext) (9 messages, latest: May 24 2023 at 02:04)
• obtain with holes (19 messages, latest: May 23 2023 at 23:43)
• missing instance in CategoryTheory.GlueData (47 messages, latest: May 23 2023 at 21:16)
• !4#4228 cannot find synthesization order for instance (9 messages, latest: May 23 2023 at 17:08)
• ✔ I'd like to help:).html) (22 messages, latest: May 23 2023 at 13:05)
• !4#4246 port Topology.TietzeExtension - maxHearbeats (7 messages, latest: May 23 2023 at 10:29)
• @\[simp\] attribute times out (14 messages, latest: May 22 2023 at 23:01)
• Conflict in Mathlib.lean (35 messages, latest: May 22 2023 at 16:19)
• DecidableEq diamond (61 messages, latest: May 22 2023 at 14:36)
• cache LinearAlgebra.Quotient (1 message, latest: May 22 2023 at 14:16)
• Rewrite fails in ite !4#4205 (7 messages, latest: May 22 2023 at 13:01)
• A translate tactic (73 messages, latest: May 22 2023 at 04:58)
• SimpNF applies scoped instance (2 messages, latest: May 22 2023 at 02:02)
• Override folder naming in mathport (1 message, latest: May 21 2023 at 22:24)
• Isolated by (3 messages, latest: May 21 2023 at 18:19)
• check all files imported (1 message, latest: May 21 2023 at 18:00)
• ✔ !4#4146 merge conflict (3 messages, latest: May 21 2023 at 15:36)
• ✔ Trouble getting mathlib (34 messages, latest: May 21 2023 at 06:40)
• Analysis.Convex.Cone.Basic (4 messages, latest: May 20 2023 at 23:09)
• !4#4047 Analysis.Normed.Group.SemiNormedGroup (10 messages, latest: May 20 2023 at 21:31)
• ✔ !4#4146 multiple defs of minimalPrimes (12 messages, latest: May 20 2023 at 20:24)
• ✔ !4#4146 port RingTheory.Ideal.MinimalPrime (24 messages, latest: May 20 2023 at 18:04)
• ✔ !4#3964 algebra.category.module.projective (13 messages, latest: May 20 2023 at 17:23)
• Rewrite failed (!4#4087 Algebra.MonoidAlgebra.ToDirectSum) (26 messages, latest: May 20 2023 at 16:58)
• Mathport failing on LittleO and BigO (2 messages, latest: May 20 2023 at 11:11)
• !4#4120 Analysis.Convex.StrictConvexSpace (11 messages, latest: May 20 2023 at 07:24)
• IR failure in example (9 messages, latest: May 19 2023 at 21:32)
• LinearAlgebra.Dual (51 messages, latest: May 19 2023 at 21:21)
• golfing the longest chain (10 messages, latest: May 19 2023 at 16:55)
• ✔ start_port: exit –> return (14 messages, latest: May 19 2023 at 16:10)
• aesop destruct side-conditions (19 messages, latest: May 19 2023 at 12:13)
• (d)simp at goal (8 messages, latest: May 18 2023 at 21:33)
• Tactic code actions (52 messages, latest: May 18 2023 at 18:40)
• library_search getting tired (39 messages, latest: May 18 2023 at 17:15)
• Shortcut to integration (30 messages, latest: May 18 2023 at 16:37)
• LocallyFIniteOrderBot (4 messages, latest: May 18 2023 at 15:56)
• !4#4083 Data.Polynomial.Expand (2 messages, latest: May 18 2023 at 13:45)
• !4#2482 Bicategory.Free (5 messages, latest: May 18 2023 at 12:34)
• tactic by (boolean?) reflection example (9 messages, latest: May 18 2023 at 10:04)
• !4#4063 RingTheory.MatrixAlgebra (3 messages, latest: May 18 2023 at 05:56)
• calc for group isos (32 messages, latest: May 17 2023 at 23:08)
• !4#3916 Algebra.Category.ModuleCat.Kernels (3 messages, latest: May 17 2023 at 16:54)
• sup/Sup (12 messages, latest: May 17 2023 at 11:58)
• ✔ trans tactic fails for equality (10 messages, latest: May 17 2023 at 09:11)
• ✔ Lint fails when installing bibtools (4 messages, latest: May 17 2023 at 08:17)
• ✔ borelize tactic !4#4018 (3 messages, latest: May 17 2023 at 05:12)
• algebra.module.localized_module (13 messages, latest: May 16 2023 at 22:06)
• invalid occurrence of universe level (47 messages, latest: May 16 2023 at 16:48)
• Auto-fixing files (13 messages, latest: May 16 2023 at 16:25)
• reenableeta !4#3414 (36 messages, latest: May 16 2023 at 14:39)
• !4#3583 comm diagram widget (9 messages, latest: May 16 2023 at 08:48)
• continuity attr on classes ineffectual (2 messages, latest: May 16 2023 at 03:48)
• "%" vs "Int.mod" (26 messages, latest: May 15 2023 at 23:53)
• coe vs val naming (4 messages, latest: May 15 2023 at 21:19)
• port Analysis.NormedSpace.OperatorNorm !4#3708 (64 messages, latest: May 15 2023 at 21:05)
• ad hoc files (7 messages, latest: May 15 2023 at 18:52)
• maintainer merge (12 messages, latest: May 15 2023 at 08:03)
• Capitalisation (3 messages, latest: May 15 2023 at 07:59)
• Bundled coercion (5 messages, latest: May 15 2023 at 05:19)
• Let's not have big files? (15 messages, latest: May 14 2023 at 15:29)
• ✔ mathlib docs locally? (2 messages, latest: May 14 2023 at 13:09)
• ✔ !4#3966 mathlib test failure (2 messages, latest: May 14 2023 at 10:03)
• how to restart port process? (7 messages, latest: May 14 2023 at 08:53)
• !4#3388 (revert porting of to_interval_mod) (33 messages, latest: May 13 2023 at 18:06)
• apply (config := { instances := false }) (3 messages, latest: May 13 2023 at 17:43)
• pp_extended_field_notation and Quiver.Hom.op (4 messages, latest: May 12 2023 at 18:45)
• porting pushforward_family (7 messages, latest: May 12 2023 at 17:57)
• port Algebra.Category.Ring.Basic !4#3901 (20 messages, latest: May 12 2023 at 16:45)
• mathlib3port [reassoc.1] (6 messages, latest: May 12 2023 at 15:05)
• Disjoint Sets proof (5 messages, latest: May 12 2023 at 11:47)
• mathlib3port error (2 messages, latest: May 12 2023 at 01:04)
• ✔ TPIL4 problem 8.5 (2 messages, latest: May 11 2023 at 20:57)
• !4#3898 simp failure (9 messages, latest: May 11 2023 at 16:24)
• ✔ PANIC index out of bounds (3 messages, latest: May 11 2023 at 04:57)
• global etaExperiment (3 messages, latest: May 10 2023 at 21:23)
• !4#3884 not on queue4 (3 messages, latest: May 10 2023 at 20:20)
• opening namespaces (5 messages, latest: May 10 2023 at 09:49)
• Github actions (7 messages, latest: May 10 2023 at 07:17)
• !4#3872 Topology.Category.Compactum (1 message, latest: May 10 2023 at 06:00)
• Qq doesn't know that two things have the same type (10 messages, latest: May 09 2023 at 22:51)
• Lake update behaviour (10 messages, latest: May 09 2023 at 14:04)
• tactic to name a ✝ variable (3 messages, latest: May 09 2023 at 09:18)
• !4#3841 Topology.Algebra.Equicontinuity (8 messages, latest: May 09 2023 at 06:51)
• continue long interpolated string on new line (7 messages, latest: May 09 2023 at 01:50)
• simp not using a simp lemma (36 messages, latest: May 08 2023 at 22:52)
• !4#3654 IsROrC (20 messages, latest: May 08 2023 at 21:44)
• rfl_without_eta (28 messages, latest: May 08 2023 at 16:30)
• Topology.ContinuousFunction.Algebra !4#3332 (2 messages, latest: May 08 2023 at 08:34)
• Hole commands MVP (1 message, latest: May 08 2023 at 08:26)
• permission for mathlib4? (6 messages, latest: May 08 2023 at 07:16)
• maxHeartbeats (21 messages, latest: May 08 2023 at 02:02)
• apply_rules with discharger (8 messages, latest: May 08 2023 at 01:12)
• termination_by in Gaussian elimination (7 messages, latest: May 07 2023 at 21:45)
• slim_check is broken (13 messages, latest: May 07 2023 at 13:11)
• library_search timeout (7 messages, latest: May 07 2023 at 08:59)
• Mathlib/Tactic.lean CI failing on master (1 message, latest: May 06 2023 at 19:05)
• Topology.Sheaves.Presheaf (1 message, latest: May 06 2023 at 17:33)
• measured lists? (25 messages, latest: May 06 2023 at 09:41)
• Slow Chinese remainder theorem (39 messages, latest: May 06 2023 at 07:39)
• Pretty-printing of sums (76 messages, latest: May 06 2023 at 01:09)
• !4#3805 (Analysis.NormedSpace.CompactOperator) (25 messages, latest: May 05 2023 at 18:09)
• linarith Preprocessor (41 messages, latest: May 05 2023 at 11:54)
• Add pi notation back ? (15 messages, latest: May 05 2023 at 11:33)
• RingTheory.Polynomial.Quotient !4#3292 (18 messages, latest: May 04 2023 at 17:55)
• linarith failing (24 messages, latest: May 04 2023 at 13:33)
• !4#3708 Analysis.NormedSpace.OperatorNorm (16 messages, latest: May 04 2023 at 06:51)
• ring vs ring_nf (18 messages, latest: May 04 2023 at 01:56)
• !4#3332 Topology.ContinuousFunction.Algebra (10 messages, latest: May 03 2023 at 16:41)
• Stepping through simp_rw (66 messages, latest: May 03 2023 at 12:53)
• git error cannot lock ref (10 messages, latest: May 03 2023 at 12:31)
• !4#3674 MeasureTheory.Measure.OuterMeasure (18 messages, latest: May 03 2023 at 09:39)
• !4#2104 simpNF error in other files (9 messages, latest: May 03 2023 at 06:40)
• mono changes? (47 messages, latest: May 03 2023 at 04:56)
• try? is the same as optional? (3 messages, latest: May 03 2023 at 01:16)
• LinearAlgebra.Determinant !4#3694 (10 messages, latest: May 03 2023 at 01:07)
• !4#3758 – rfl refactor & fix (37 messages, latest: May 02 2023 at 19:30)
• linarith bug (8 messages, latest: May 02 2023 at 03:30)
• analyzing the definition of Substring.next (6 messages, latest: May 02 2023 at 01:00)
• !4#3360 OrderDual (12 messages, latest: May 01 2023 at 16:39)
• typeclass inference failure (12 messages, latest: May 01 2023 at 11:51)
• More universe weirdness (7 messages, latest: May 01 2023 at 10:41)
• change in behaviour with simps (2 messages, latest: May 01 2023 at 09:34)
• library_search regression (10 messages, latest: May 01 2023 at 07:00)
• Array (56 messages, latest: Apr 30 2023 at 17:21)
• !4#3649 RingTheory.TensorProduct (2 messages, latest: Apr 30 2023 at 11:06)
• learning what a left Kan extension is (34 messages, latest: Apr 30 2023 at 10:26)
• Basic expr functions (9 messages, latest: Apr 30 2023 at 09:05)
• String.drop and String.popn are the same (8 messages, latest: Apr 30 2023 at 06:36)
• ✔ ring tactic cannot prove equality about MvPolynomial (12 messages, latest: Apr 30 2023 at 04:21)
• !4#3716 FieldTheory.Tower (12 messages, latest: Apr 29 2023 at 11:18)
• PSA: broken diff selection on github (3 messages, latest: Apr 29 2023 at 10:02)
• !4#3225 porting MvPolynomial.Funext (5 messages, latest: Apr 29 2023 at 05:10)
• instant library_search (84 messages, latest: Apr 28 2023 at 23:41)
• Cache and MathlibExtras (5 messages, latest: Apr 28 2023 at 23:35)
• library_search with maxHeartbeats 0 (2 messages, latest: Apr 28 2023 at 21:52)
• alias is noncomputable (4 messages, latest: Apr 28 2023 at 20:54)
• ✔ mathlib4 docs website strange behaviour (6 messages, latest: Apr 28 2023 at 19:45)
• !4#3710 LinearAlgebra.Matrix.SpecialLinearGroup (21 messages, latest: Apr 28 2023 at 17:34)
• bugs and issues in the Data.List.Infix port (5 messages, latest: Apr 28 2023 at 16:49)
• exists_prop (26 messages, latest: Apr 28 2023 at 16:23)
• simpa (4 messages, latest: Apr 28 2023 at 15:58)
• !4#3705 (Topology.Category.Profinite.Basic) (7 messages, latest: Apr 28 2023 at 15:00)
• propose on a product space (1 message, latest: Apr 28 2023 at 14:49)
• !4#3664 Topology.Algebra.UniformConvergence (49 messages, latest: Apr 28 2023 at 08:02)
• !4#2778 (7 messages, latest: Apr 28 2023 at 06:14)
• !4#3684 Topology.Algebra.Module.StrongTopology (6 messages, latest: Apr 27 2023 at 20:52)
• !4#3761 LinearAlgebra.Matrix.Zpow (7 messages, latest: Apr 27 2023 at 12:36)
• !4#3552 (LinearAlgebra.Matrix.ToLin) (6 messages, latest: Apr 27 2023 at 11:03)
• !4#3510 CategoryTheory.Simple (4 messages, latest: Apr 26 2023 at 15:55)
• Starting a project with Mathlib4 dependency fails… (30 messages, latest: Apr 26 2023 at 13:52)
• !4#3487 last minute split? (6 messages, latest: Apr 26 2023 at 12:34)
• LinearAlgebra.Matrix.ToLin !4#3552 (13 messages, latest: Apr 26 2023 at 11:00)
• !4#3484, Analysis.Seminorm (38 messages, latest: Apr 26 2023 at 04:57)
• Porting goals for Copenhagen master class (6 messages, latest: Apr 25 2023 at 23:32)
• priority 900 (2 messages, latest: Apr 25 2023 at 23:25)
• mathport root (22 messages, latest: Apr 25 2023 at 13:30)
• to_additive speedup (1 message, latest: Apr 24 2023 at 17:54)
• !4#3622 Analysis.Convex.Jensen (4 messages, latest: Apr 24 2023 at 13:29)
• mathport drops priorities in attribute \[instance\] (21 messages, latest: Apr 24 2023 at 13:01)
• Instance cache weirdness (19 messages, latest: Apr 24 2023 at 12:08)
• !4#3466 LinearAlgebra.FiniteDimensional (16 messages, latest: Apr 24 2023 at 11:41)
• filter_upwards spacing (4 messages, latest: Apr 24 2023 at 09:34)
• Placeholder in obtain (1 message, latest: Apr 24 2023 at 08:12)
• how should I merge old & new copyright headers? (7 messages, latest: Apr 24 2023 at 02:10)
• new lake gives me way too much information (7 messages, latest: Apr 23 2023 at 21:27)
• dsimp only for universal cleanup (64 messages, latest: Apr 23 2023 at 16:52)
• pp.beta (14 messages, latest: Apr 23 2023 at 12:20)
• Force push (25 messages, latest: Apr 23 2023 at 08:23)
• ext issues (22 messages, latest: Apr 22 2023 at 17:07)
• doc-gen duration (31 messages, latest: Apr 22 2023 at 10:49)
• bug in apply_fun (13 messages, latest: Apr 22 2023 at 10:09)
• !4#3578 (3 messages, latest: Apr 22 2023 at 01:25)
• performance debug (107 messages, latest: Apr 21 2023 at 16:48)
• !4#3360 new ext lemma generation (10 messages, latest: Apr 21 2023 at 16:07)
• Labelling abuse (40 messages, latest: Apr 21 2023 at 15:31)
• porting Data.RBTree.Init (13 messages, latest: Apr 21 2023 at 15:31)
• induction in mathlib4 (17 messages, latest: Apr 21 2023 at 13:21)
• Cache failures with the Lean bump (18 messages, latest: Apr 21 2023 at 13:00)
• Nontrivial typeclass def-eqs (7 messages, latest: Apr 20 2023 at 17:51)
• apply_with … { instances := false } (14 messages, latest: Apr 20 2023 at 17:15)
• turn off type of proof in infoview (8 messages, latest: Apr 20 2023 at 16:37)
• Suggestions for #port-dashboard (122 messages, latest: Apr 20 2023 at 11:43)
• failure of dot notation (26 messages, latest: Apr 20 2023 at 07:57)
• failure of dot notation in infoview (1 message, latest: Apr 20 2023 at 07:57)
• !4#3215 and data.matrix.notation (77 messages, latest: Apr 20 2023 at 04:47)
• New propose tactic (32 messages, latest: Apr 20 2023 at 04:41)
• Bug in reassoc? (26 messages, latest: Apr 20 2023 at 00:49)
• !4#3434 (6 messages, latest: Apr 19 2023 at 17:07)
• ✔ getting started with porting (8 messages, latest: Apr 19 2023 at 02:43)
• stack overflow in cache get (13 messages, latest: Apr 18 2023 at 18:06)
• Aesop and cases (9 messages, latest: Apr 18 2023 at 13:25)
• !4#3490 Urysohns Lemma (9 messages, latest: Apr 18 2023 at 03:17)
• push_neg of \and (10 messages, latest: Apr 18 2023 at 02:54)
• !4#3472, GroupTheory.Perm.Cycle.Concrete (1 message, latest: Apr 17 2023 at 06:25)
• ✔ Sharing mathlib4 between several projects (6 messages, latest: Apr 16 2023 at 21:53)
• Universe issues with concrete categories (38 messages, latest: Apr 16 2023 at 21:46)
• #aligning Hom.val (1 message, latest: Apr 16 2023 at 12:16)
• !4#3208 merge conflicts (12 messages, latest: Apr 16 2023 at 11:10)
• A twist on obtain (11 messages, latest: Apr 15 2023 at 19:56)
• ext debugging (23 messages, latest: Apr 15 2023 at 17:13)
• Fixing Finset.induction (5 messages, latest: Apr 15 2023 at 16:49)
• ✔ List.sum distributivity (13 messages, latest: Apr 15 2023 at 00:27)
• flamegraphs (29 messages, latest: Apr 14 2023 at 16:01)
• import Mathlib causes simp to fail to recognize match (27 messages, latest: Apr 14 2023 at 11:35)
• Type class inference problem (1 message, latest: Apr 14 2023 at 09:26)
• unquoteExpr: inst✝².2 : Expr (14 messages, latest: Apr 14 2023 at 08:20)
• irreducible_def (21 messages, latest: Apr 14 2023 at 06:36)
• Dead names (15 messages, latest: Apr 13 2023 at 20:10)
• Coarseness of Mathlib.Cache (4 messages, latest: Apr 13 2023 at 19:29)
• porters (42 messages, latest: Apr 13 2023 at 14:37)
• simps (3 messages, latest: Apr 12 2023 at 21:53)
• !4#3082 (18 messages, latest: Apr 12 2023 at 12:52)
• !4#3392 (7 messages, latest: Apr 12 2023 at 10:04)
• names distinguished only by case (98 messages, latest: Apr 11 2023 at 21:53)
• Analysis.NormedSpace.Basic !4#3280 (30 messages, latest: Apr 11 2023 at 21:10)
• !4#2148 (47 messages, latest: Apr 11 2023 at 18:20)
• New mathlib4 porting PRs by new people (13 messages, latest: Apr 11 2023 at 17:42)
• rel_embedding.coe_coe_fn (6 messages, latest: Apr 11 2023 at 09:03)
• Fintype (alternatingGroup α) (41 messages, latest: Apr 10 2023 at 14:39)
• bug in rw tactic? (1 message, latest: Apr 09 2023 at 18:56)
• wlog #16495 (150 messages, latest: Apr 09 2023 at 08:33)
• Porting Data.String.Basic (64 messages, latest: Apr 08 2023 at 15:32)
• logic.equiv.basic (24 messages, latest: Apr 08 2023 at 11:32)
• Topology.MetricSpace.Closeds !4#3338 (1 message, latest: Apr 08 2023 at 09:51)
• Preferring homogeneous operators (1 message, latest: Apr 08 2023 at 07:19)
• Data.Nat.Choose.Multinomial (5 messages, latest: Apr 07 2023 at 19:04)
• !4#3170 (3 messages, latest: Apr 07 2023 at 17:25)
• CoeFun instance not found? (113 messages, latest: Apr 07 2023 at 14:04)
• No decidability for structure (17 messages, latest: Apr 06 2023 at 23:10)
• !4#3312 (8 messages, latest: Apr 06 2023 at 18:25)
• 10 million heartbeats (!4#3242) (19 messages, latest: Apr 06 2023 at 11:50)
• !4#3287 (5 messages, latest: Apr 05 2023 at 14:00)
• auto-coercion hell (21 messages, latest: Apr 05 2023 at 08:41)
• !4#3274 typeclass instance problem (11 messages, latest: Apr 05 2023 at 05:38)
• mathlib4 bot (8 messages, latest: Apr 05 2023 at 00:02)
• import tactic (44 messages, latest: Apr 04 2023 at 23:37)
• !4#3258 ext error (5 messages, latest: Apr 04 2023 at 11:17)
• Another FunLike issue, with linear maps (5 messages, latest: Apr 04 2023 at 09:39)
• !4#3187 (Data.Seq.Seq) (14 messages, latest: Apr 04 2023 at 03:13)
• module doc for Data.ZMod.Defs (1 message, latest: Apr 04 2023 at 03:11)
• semicolon (9 messages, latest: Apr 03 2023 at 18:35)
• !4#3051 AffineSpace.Combination (36 messages, latest: Apr 03 2023 at 14:26)
• mangled docstring for docs4#congrArg (2 messages, latest: Apr 03 2023 at 12:33)
• !4#3225 (19 messages, latest: Apr 02 2023 at 19:59)
• !4#3232 (1 message, latest: Apr 02 2023 at 18:55)
• field_simp (11 messages, latest: Apr 02 2023 at 16:57)
• Bug in polyrith? (44 messages, latest: Apr 02 2023 at 03:03)
• headI and getLastI (4 messages, latest: Apr 01 2023 at 09:17)
• alias & protected (12 messages, latest: Apr 01 2023 at 09:15)
• !4#3209 (2 messages, latest: Apr 01 2023 at 03:49)
• derive_fintype (38 messages, latest: Apr 01 2023 at 01:46)
• Failing to infer Module instance from Algebra (14 messages, latest: Mar 31 2023 at 22:22)
• permission (4 messages, latest: Mar 31 2023 at 21:30)
• !4#3206 (3 messages, latest: Mar 31 2023 at 17:50)
• !4#3192 (3 messages, latest: Mar 31 2023 at 13:59)
• !4#2977 Algebra.DirectSum.TensorProduct (29 messages, latest: Mar 30 2023 at 20:32)
• What does export do in Lean3 (10 messages, latest: Mar 30 2023 at 17:00)
• simp on defs (lean4#2042) (12 messages, latest: Mar 30 2023 at 15:36)
• !4#3165 (46 messages, latest: Mar 30 2023 at 07:56)
• ✔ prefix docblame (6 messages, latest: Mar 30 2023 at 07:00)
• dsimp took 83.3s (24 messages, latest: Mar 29 2023 at 19:56)
• !4#3168 (42 messages, latest: Mar 29 2023 at 17:40)
• !4#3169 (6 messages, latest: Mar 29 2023 at 10:28)
• Introducing all dependent variables (69 messages, latest: Mar 29 2023 at 03:57)
• unexpanders for functors (39 messages, latest: Mar 29 2023 at 01:30)
• !4#3157 (5 messages, latest: Mar 28 2023 at 18:25)
• simp only does decidable checks? (10 messages, latest: Mar 28 2023 at 05:52)
• finishing up ofScientific in norm_num (68 messages, latest: Mar 28 2023 at 04:12)
• naming bikeshed: mkpair/unpair (15 messages, latest: Mar 28 2023 at 03:39)
• How easy is an easy PR? (35 messages, latest: Mar 27 2023 at 23:05)
• how does changing imports affect tc synthesis (30 messages, latest: Mar 27 2023 at 19:38)
• failing cases for continuity (20 messages, latest: Mar 27 2023 at 16:05)
• !4#3039 or backport first? (1 message, latest: Mar 27 2023 at 13:53)
• ≤, ≥, and ∈ symbols are duplicated in docs4 (18 messages, latest: Mar 27 2023 at 13:38)
• data.set.pairwise.basic (6 messages, latest: Mar 27 2023 at 10:12)
• Elided props in binders (4 messages, latest: Mar 27 2023 at 09:28)
• Strict-implicit binder with existential (9 messages, latest: Mar 27 2023 at 08:20)
• !4#3113 (4 messages, latest: Mar 27 2023 at 06:36)
• forward porting (55 messages, latest: Mar 27 2023 at 02:02)
• !4#3115 (4 messages, latest: Mar 27 2023 at 01:09)
• !4#3106 (21 messages, latest: Mar 27 2023 at 00:03)
• !4#3107 (59 messages, latest: Mar 26 2023 at 18:58)
• !4#2986 Maschke theorem (5 messages, latest: Mar 26 2023 at 11:22)
• making pr in mathlib4 (21 messages, latest: Mar 25 2023 at 23:25)
• instructions for forward porting mathlib3 changes (24 messages, latest: Mar 25 2023 at 21:39)
• coe_degree for simple graphs (3 messages, latest: Mar 25 2023 at 20:46)
• tc synthesis repeatedly tries the last one on the list (8 messages, latest: Mar 25 2023 at 19:37)
• ✔ installing mathlib4 (3 messages, latest: Mar 25 2023 at 18:48)
• Syntax for unpacking structures (66 messages, latest: Mar 24 2023 at 20:56)
• count_eq_card_filter_eq (30 messages, latest: Mar 24 2023 at 20:29)
• simps generates invalid simp lemma (6 messages, latest: Mar 24 2023 at 20:29)
• !4#3068 (27 messages, latest: Mar 24 2023 at 19:03)
• type resolution issue in !4#3043 (6 messages, latest: Mar 24 2023 at 17:33)
• !4#3001 (7 messages, latest: Mar 24 2023 at 16:06)
• List.perm_comm at Data.List.Perm (2 messages, latest: Mar 24 2023 at 14:30)
• Goal state not updating, bugs, etc. (115 messages, latest: Mar 24 2023 at 10:30)
• OrderIso toFun (7 messages, latest: Mar 23 2023 at 20:27)
• !4#2969 (7 messages, latest: Mar 23 2023 at 17:12)
• symm with Ne (4 messages, latest: Mar 23 2023 at 16:46)
• ext tactic intros too few variables (12 messages, latest: Mar 23 2023 at 14:58)
• Noncomputable definitions in !4#3007 (61 messages, latest: Mar 23 2023 at 10:59)
• decidability leakage (95 messages, latest: Mar 22 2023 at 17:19)
• dsimp and Iff.rfl (13 messages, latest: Mar 22 2023 at 15:20)
• Aesop and Lambdas (28 messages, latest: Mar 22 2023 at 02:13)
• push_cast TODO (1 message, latest: Mar 21 2023 at 23:45)
• ✔ unknown package 'Mathlib' (6 messages, latest: Mar 21 2023 at 21:51)
• push_cast and OfScientific (5 messages, latest: Mar 21 2023 at 15:11)
• Suggestions for #port-status (1 message, latest: Mar 21 2023 at 12:31)
• Slowly-failing solve-by-elim call (34 messages, latest: Mar 21 2023 at 10:08)
• using etaExperiment (17 messages, latest: Mar 20 2023 at 20:29)
• lift duplicates a hypothesis (2 messages, latest: Mar 20 2023 at 17:14)
• clear_value (18 messages, latest: Mar 20 2023 at 10:03)
• !4#2894 (27 messages, latest: Mar 19 2023 at 23:15)
• !4#2994 (3 messages, latest: Mar 19 2023 at 20:44)
• Status of !4#2470 (SetTheory.Ordinal.Notation) (64 messages, latest: Mar 19 2023 at 18:25)
• Old PRs (3 messages, latest: Mar 19 2023 at 16:35)
• coercion from PNat to Nat is not reducing (11 messages, latest: Mar 19 2023 at 14:54)
• Out of sync files (42 messages, latest: Mar 19 2023 at 13:05)
• !4#2983 #port-dashboard race condition (12 messages, latest: Mar 19 2023 at 11:51)
• =Q vs. isDefEq in norm_num (3 messages, latest: Mar 19 2023 at 00:27)
• Lean 4 setup help (10 messages, latest: Mar 18 2023 at 22:49)
• Explicit naming (3 messages, latest: Mar 18 2023 at 11:40)
• elementwise (5 messages, latest: Mar 17 2023 at 17:02)
• tfae naming (6 messages, latest: Mar 17 2023 at 15:34)
• to_additive generates nonsense names for Prod instances (8 messages, latest: Mar 17 2023 at 14:10)
• intros equivalent (14 messages, latest: Mar 17 2023 at 11:15)
• Complex.Basic (56 messages, latest: Mar 17 2023 at 10:45)
• ##18596 (9 messages, latest: Mar 17 2023 at 10:21)
• std bump (2 messages, latest: Mar 17 2023 at 10:19)
• !4#2850 (51 messages, latest: Mar 16 2023 at 23:04)
• (deterministic) timeout at 'whnf', maximum number of heartbe (1 message, latest: Mar 16 2023 at 22:21)
• CI loops (1 message, latest: Mar 16 2023 at 19:41)
• crash (21 messages, latest: Mar 16 2023 at 17:26)
• simp doesn't work without placeholders (9 messages, latest: Mar 16 2023 at 17:16)
• !4#2931 (6 messages, latest: Mar 16 2023 at 17:04)
• speeding up linting (10 messages, latest: Mar 16 2023 at 14:22)
• !4#2868 (24 messages, latest: Mar 16 2023 at 13:58)
• Decidability of < when constructing LinearOrder via lift' (5 messages, latest: Mar 16 2023 at 08:59)
• !4#2887 Data.MvPolynomial.Monad (18 messages, latest: Mar 15 2023 at 23:37)
• Forward porting #17483 / !4#2884 (22 messages, latest: Mar 15 2023 at 17:46)
• @eq.drec_on in Lean 4 (!4#2194) (10 messages, latest: Mar 15 2023 at 16:55)
• !4#2692 AffineEquiv (22 messages, latest: Mar 15 2023 at 12:08)
• porting CategoryTheory.ConcreteCategory.BundledHom (2 messages, latest: Mar 15 2023 at 12:00)
• tactic documentation (15 messages, latest: Mar 15 2023 at 10:26)
• A new tactic (43 messages, latest: Mar 15 2023 at 09:26)
• Tactic porting assignments (392 messages, latest: Mar 15 2023 at 08:56)
• potential improvements to library_search (29 messages, latest: Mar 15 2023 at 00:07)
• simp normal form: ofNat or Nat.cast? (32 messages, latest: Mar 14 2023 at 23:46)
• failing simps (2 messages, latest: Mar 14 2023 at 19:19)
• Problem with linarith (4 messages, latest: Mar 14 2023 at 18:13)
• RingTheory.Ideal.Prod !4#2877 (5 messages, latest: Mar 14 2023 at 15:57)
• Removing notation for Function.combine (5 messages, latest: Mar 14 2023 at 12:51)
• Ord ɑ from LinearOrder ɑ? (19 messages, latest: Mar 14 2023 at 10:24)
• !4#2797 / !4#2769 (129 messages, latest: Mar 14 2023 at 07:25)
• Making variable in class field explicit (20 messages, latest: Mar 14 2023 at 06:49)
• Addressing porting notes? (4 messages, latest: Mar 14 2023 at 01:41)
• change at (28 messages, latest: Mar 13 2023 at 23:07)
• Data.Complex.Exponential !4#2785 (11 messages, latest: Mar 13 2023 at 20:20)
• can't infer ContinuousNeg (5 messages, latest: Mar 13 2023 at 19:43)
• ✔ congr_prop ? (15 messages, latest: Mar 13 2023 at 19:34)
• RingTheory.Finiteness !4#2811 (9 messages, latest: Mar 13 2023 at 18:00)
• ((2 : ℤ) : R) = 2 (18 messages, latest: Mar 13 2023 at 15:57)
• Forward-porting #18543? (3 messages, latest: Mar 13 2023 at 15:45)
• !4#2792 Analysis.Normed.Field.Basic (9 messages, latest: Mar 13 2023 at 15:05)
• !4#2832 (12 messages, latest: Mar 13 2023 at 14:36)
• Issues in !4#2788 (LinearAlgebra.Smodeq) (17 messages, latest: Mar 13 2023 at 05:13)
• PR permission (3 messages, latest: Mar 13 2023 at 03:44)
• Forward porting #17483 (9 messages, latest: Mar 12 2023 at 23:51)
• Naming of PreservesFiniteLimits.PreservesFiniteLimits (19 messages, latest: Mar 12 2023 at 17:57)
• !4#2798 simpNF (39 messages, latest: Mar 12 2023 at 14:12)
• Updating mathlib4 (8 messages, latest: Mar 12 2023 at 12:26)
• transitivity vs. trans? (2 messages, latest: Mar 12 2023 at 12:13)
• !4#2821 (18 messages, latest: Mar 12 2023 at 11:15)
• !4#2763 RingTheory.Localization.FractionRing (6 messages, latest: Mar 12 2023 at 09:44)
• congr and subsingleton.elim (33 messages, latest: Mar 11 2023 at 17:42)
• noncomputable bug? (1 message, latest: Mar 11 2023 at 15:44)
• !4#2790 rfl failure (11 messages, latest: Mar 11 2023 at 15:31)
• !4#2773 type mismatch (52 messages, latest: Mar 11 2023 at 14:41)
• failed to synthesize instance Applicative id (12 messages, latest: Mar 11 2023 at 09:47)
• LinearAlgebra.QuotientPi !4#2378 (9 messages, latest: Mar 11 2023 at 07:20)
• porting multiequalizers (16 messages, latest: Mar 10 2023 at 22:53)
• ✔ Type class inference in category theory (9 messages, latest: Mar 10 2023 at 21:01)
• !4#2755 Topology.PathConnected (1 message, latest: Mar 10 2023 at 20:38)
• fix-comments.py on windows (5 messages, latest: Mar 10 2023 at 20:34)
• ofReal_two (20 messages, latest: Mar 10 2023 at 19:31)
• simps generates useless lemmas (4 messages, latest: Mar 10 2023 at 17:58)
• @\[simps!\] unfolds type (8 messages, latest: Mar 10 2023 at 13:32)
• ✔ Porting for newbies (75 messages, latest: Mar 10 2023 at 11:35)
• universe issue (16 messages, latest: Mar 10 2023 at 08:46)
• bug in ext? (16 messages, latest: Mar 10 2023 at 05:25)
• reassoc_of (20 messages, latest: Mar 10 2023 at 04:19)
• ✔ n ≠ 0 → n ≥ 1 (13 messages, latest: Mar 10 2023 at 04:18)
• Try this: ring_nf (18 messages, latest: Mar 10 2023 at 02:19)
• hygenic reassoc (4 messages, latest: Mar 09 2023 at 21:13)
• troubleshooting to_additive (31 messages, latest: Mar 09 2023 at 18:15)
• @[simp] on equation compiler definitions (66 messages, latest: Mar 09 2023 at 17:56)
• making variables implicit (12 messages, latest: Mar 09 2023 at 16:51)
• aesop replaces obviously? (7 messages, latest: Mar 09 2023 at 14:53)
• NormedAddGroupHom coercion (4 messages, latest: Mar 09 2023 at 14:15)
• Default OfScientific instance (6 messages, latest: Mar 09 2023 at 09:49)
• ring_nf failing to fully normalize (19 messages, latest: Mar 09 2023 at 00:55)
• ✔ cast_sub in ring (12 messages, latest: Mar 09 2023 at 00:52)
• moving RatCast to Std (27 messages, latest: Mar 08 2023 at 20:06)
• Nat.cast to WithBot (7 messages, latest: Mar 08 2023 at 18:15)
• Issue in !4#2702 (Topology.UniformSpace.CompareReals) (33 messages, latest: Mar 08 2023 at 16:54)
• !4#2438 higher_order attribute (2 messages, latest: Mar 08 2023 at 13:23)
• bug in linarith (15 messages, latest: Mar 08 2023 at 07:43)
• stack overflow in linarith (4 messages, latest: Mar 08 2023 at 07:38)
• Dfinsupp.Lex (9 messages, latest: Mar 08 2023 at 06:29)
• bug in positivity? (36 messages, latest: Mar 08 2023 at 01:31)
• linter crash (9 messages, latest: Mar 08 2023 at 00:17)
• ✔ nat.prime norm_num regression? (7 messages, latest: Mar 07 2023 at 11:53)
• ✔ Problems building mathlib4 (37 messages, latest: Mar 06 2023 at 18:16)
• CoeTC typeclass (8 messages, latest: Mar 06 2023 at 10:56)
• ✔ 10^n ≥ 10 (10 messages, latest: Mar 06 2023 at 09:22)
• Bug in ring1? (14 messages, latest: Mar 06 2023 at 05:20)
• Bug in ring_nf? (8 messages, latest: Mar 06 2023 at 00:18)
• Issues in !4#2530 (Combinatorics.Derangements.Basic) (51 messages, latest: Mar 05 2023 at 23:01)
• eta ftw (38 messages, latest: Mar 05 2023 at 10:57)
• ✔ To the power of intereger (14 messages, latest: Mar 04 2023 at 21:07)
• New-style dot notation and pi types (10 messages, latest: Mar 04 2023 at 05:17)
• linarith and ENNReal (10 messages, latest: Mar 03 2023 at 20:59)
• pseudo_metric_space.edist_dist_tac (13 messages, latest: Mar 03 2023 at 18:35)
• eq_true_iff (1 message, latest: Mar 03 2023 at 17:37)
• neg_mem_iff (8 messages, latest: Mar 03 2023 at 10:17)
• CategoryTheory.PathCategory (54 messages, latest: Mar 03 2023 at 08:49)
• Algebra.Algebra.Operations !4#2568 (7 messages, latest: Mar 03 2023 at 08:06)
• ✔ ∃ injective implies ∃ surjective (11 messages, latest: Mar 03 2023 at 00:18)
• ✔ Cannot go to definition (13 messages, latest: Mar 02 2023 at 20:20)
• ✔ Hypertactic? (5 messages, latest: Mar 02 2023 at 14:44)
• two errors (28 messages, latest: Mar 02 2023 at 13:15)
• Single issue in !4##2565 Combinatorics.SimpleGraph.Prod (9 messages, latest: Mar 02 2023 at 10:39)
• TC extends vs instance-implicit binders (18 messages, latest: Mar 02 2023 at 08:09)
• CategoryTheory.Quotient (!4#2339) (13 messages, latest: Mar 02 2023 at 06:47)
• Topology.Algebra.Ring (1 message, latest: Mar 02 2023 at 04:56)
• CoeFun (39 messages, latest: Mar 01 2023 at 19:58)
• instance search timeouts in !4#2547 (6 messages, latest: Mar 01 2023 at 19:55)
• rcases question (21 messages, latest: Mar 01 2023 at 19:46)
• Coercions in Mathlib4 vs Mathlib3 (18 messages, latest: Mar 01 2023 at 18:12)
• PANIC …contains rhs (15 messages, latest: Mar 01 2023 at 17:35)
• PSA: using Aesop for auto-params (3 messages, latest: Mar 01 2023 at 17:02)
• case_bash and automation (21 messages, latest: Mar 01 2023 at 16:39)
• Help with simpNF linter (22 messages, latest: Mar 01 2023 at 09:27)
• enthusiastic push_cast (7 messages, latest: Mar 01 2023 at 04:12)
• unsupported: ambiguous notation (18 messages, latest: Feb 28 2023 at 19:08)
• !4#2447 Sum.Associator (2 messages, latest: Feb 28 2023 at 18:04)
• {Finset,Multiset}.Basic changes from mathlib3 !4#1726 (15 messages, latest: Feb 28 2023 at 16:02)
• Skip sorry for a while to work on another dependent file (1 message, latest: Feb 28 2023 at 11:12)
• references.bib (2 messages, latest: Feb 27 2023 at 23:50)
• Status of !4#2526 Combinatorics.SimpleGraph.Coloring (2 messages, latest: Feb 27 2023 at 20:27)
• What to call primrec.not in mathlib 4 (5 messages, latest: Feb 27 2023 at 17:03)
• Algebra.BigOperators.Finprod mathlib4#1766 (21 messages, latest: Feb 27 2023 at 14:00)
• why (or why not) aesop? (5 messages, latest: Feb 27 2023 at 11:13)
• ✔ Tactic for fraction cancellation (99 messages, latest: Feb 27 2023 at 01:11)
• Neg ℕ when looking for zpow (10 messages, latest: Feb 26 2023 at 23:07)
• simp not simplifying definition (6 messages, latest: Feb 26 2023 at 22:04)
• Algebra.Order.Hom.Ring #1482 (7 messages, latest: Feb 26 2023 at 16:07)
• Proving elementary-algebra identities: now or later? (5 messages, latest: Feb 26 2023 at 15:58)
• Help requested for !4#2458 (GroupTheory.Perm.Sign) (10 messages, latest: Feb 26 2023 at 01:25)
• Missaligned type between Lean 3 and Lean 4 with ∃ (11 messages, latest: Feb 25 2023 at 19:47)
• Proving theorems about match (13 messages, latest: Feb 25 2023 at 14:51)
• Create typeclass goals with apply? (8 messages, latest: Feb 24 2023 at 18:58)
• analogue of local tidy attribute (24 messages, latest: Feb 24 2023 at 17:22)
• interval_cases for PNat (15 messages, latest: Feb 24 2023 at 10:08)
• bump to 2023-02-22 (6 messages, latest: Feb 24 2023 at 08:21)
• simp not full clearing goals in !4#2458 (8 messages, latest: Feb 23 2023 at 22:14)
• ressoc (attr := simp) (16 messages, latest: Feb 23 2023 at 19:46)
• simps + Trans (18 messages, latest: Feb 23 2023 at 14:36)
• Porting Logic.Equiv.Array for Primrec (4 messages, latest: Feb 23 2023 at 08:34)
• How to deal with conflicting namespaces (3 messages, latest: Feb 23 2023 at 05:42)
• !4#2457 (1 message, latest: Feb 23 2023 at 00:52)
• Splitting the mathlib4 stream (9 messages, latest: Feb 23 2023 at 00:30)
• lean 3 ignores ascription of function (13 messages, latest: Feb 22 2023 at 20:41)
• Data.Array.Lemmas PR !4#2194 (13 messages, latest: Feb 22 2023 at 18:54)
• Commute.nat_cast_left (4 messages, latest: Feb 22 2023 at 14:52)
• !4#2400 Analysis.Normed.Group.Seminorm (1 message, latest: Feb 22 2023 at 06:08)
• refactoring mathport syntax? (7 messages, latest: Feb 22 2023 at 03:48)
• rename_i during porting (21 messages, latest: Feb 22 2023 at 03:24)
• Linear map diamond? (8 messages, latest: Feb 22 2023 at 02:53)
• invalid 'simp' G ≃ₜ G in !4#2420 (16 messages, latest: Feb 22 2023 at 02:51)
• ext/funext (3 messages, latest: Feb 22 2023 at 02:21)
• simp [← mylemma] (22 messages, latest: Feb 22 2023 at 00:43)
• CategoryTheory.Adjunction.Opposites !4#2424 (2 messages, latest: Feb 22 2023 at 00:26)
• contrapose! this (62 messages, latest: Feb 21 2023 at 17:52)
• Print coercions explicitly (4 messages, latest: Feb 21 2023 at 17:41)
• unused universe parameter (21 messages, latest: Feb 21 2023 at 17:14)
• GroupTheory.OrderOfElement !4#2279 (13 messages, latest: Feb 21 2023 at 15:52)
• LinearAlgebra.Prod !4#2415 (18 messages, latest: Feb 21 2023 at 15:27)
• module R R (4 messages, latest: Feb 21 2023 at 11:38)
• Issue in !4#2409: index is not a variable (1 message, latest: Feb 21 2023 at 05:15)
• how to use the mathlib cache? (19 messages, latest: Feb 20 2023 at 23:40)
• print simp set (11 messages, latest: Feb 20 2023 at 18:04)
• Port Status Webpage (50 messages, latest: Feb 20 2023 at 17:46)
• Fintype.card of a Set ℕ (8 messages, latest: Feb 20 2023 at 16:07)
• inefficient projections (12 messages, latest: Feb 20 2023 at 15:43)
• simp failure in !4#2390 (1 message, latest: Feb 20 2023 at 08:52)
• [reassoc] issue (8 messages, latest: Feb 19 2023 at 23:14)
• repo access (10 messages, latest: Feb 19 2023 at 18:51)
• inductionOn vs induction_on (9 messages, latest: Feb 19 2023 at 17:25)
• simpNF issues in Computability.RegularExpressions !4#2306 (20 messages, latest: Feb 19 2023 at 16:25)
• Algebra.Algebra.Basic (25 messages, latest: Feb 19 2023 at 14:28)
• Coercion from NNReal to ENNReal (2 messages, latest: Feb 19 2023 at 01:06)
• def .. deriving (1 message, latest: Feb 18 2023 at 22:41)
• duplicated namespace (88 messages, latest: Feb 18 2023 at 22:29)
• mixin algebraic typeclasses (113 messages, latest: Feb 18 2023 at 20:20)
• LinearAlgebra.Quotient !4#2286 (20 messages, latest: Feb 18 2023 at 20:00)
• Issues in !4a#2353 (SetTheory.Ordinal.NaturalOps) (4 messages, latest: Feb 18 2023 at 06:22)
• ✔ Mathlib build fails (2 messages, latest: Feb 17 2023 at 23:09)
• OrderTopology without LinearOrder (2 messages, latest: Feb 17 2023 at 21:37)
• stickers/logo (6 messages, latest: Feb 17 2023 at 12:17)
• failed synth instance (5 messages, latest: Feb 17 2023 at 11:02)
• delete mathport syntax when porting? (4 messages, latest: Feb 17 2023 at 08:45)
• namespacing mathport syntax? (2 messages, latest: Feb 16 2023 at 23:53)
• CategoryTheory.Monoidal.Category (1 message, latest: Feb 16 2023 at 22:52)
• CategoryTheory.Adjunction.Basic (26 messages, latest: Feb 16 2023 at 21:20)
• renaming incorrect names? (4 messages, latest: Feb 16 2023 at 20:48)
• aligning Bicategory fields (3 messages, latest: Feb 16 2023 at 18:51)
• new name for Cauchy (14 messages, latest: Feb 16 2023 at 15:19)
• set_theory.ordinal.arithmetic !4#2271 (16 messages, latest: Feb 16 2023 at 08:48)
• old/new structures (19 messages, latest: Feb 16 2023 at 05:26)
• typeclass instance issues in !4#2280 (3 messages, latest: Feb 16 2023 at 05:24)
• Newline in #align (6 messages, latest: Feb 16 2023 at 05:04)
• CategoryTheory.Bicategory.Functor !4#2301 (3 messages, latest: Feb 15 2023 at 21:12)
• data.fintype.card_embedding !4#2166 (51 messages, latest: Feb 15 2023 at 14:42)
• number of unported dependencies (3 messages, latest: Feb 15 2023 at 14:36)
• ✔ Finset Repr is unsafe (22 messages, latest: Feb 15 2023 at 13:52)
• local homeomorph (5 messages, latest: Feb 15 2023 at 12:29)
• dot notation with implicit args (5 messages, latest: Feb 15 2023 at 06:52)
• isDefEq not transitive? (14 messages, latest: Feb 15 2023 at 06:44)
• mathport bug with ^ (10 messages, latest: Feb 15 2023 at 00:49)
• bug in refine or apply_fun (9 messages, latest: Feb 14 2023 at 23:41)
• HPow (6 messages, latest: Feb 14 2023 at 21:22)
• mathport fails after mathlib4 update (18 messages, latest: Feb 14 2023 at 19:58)
• type class inference fails at unification? (13 messages, latest: Feb 14 2023 at 19:34)
• Tracing simp that timeouts (12 messages, latest: Feb 14 2023 at 19:27)
• linear_algebra.finsupp !4#2277 (1 message, latest: Feb 14 2023 at 19:05)
• simps and simpNF linter (10 messages, latest: Feb 14 2023 at 14:21)
• LinearAlgebra.Span !4#2248 (10 messages, latest: Feb 14 2023 at 13:52)
• GroupTheory.Index !4#2222 (12 messages, latest: Feb 14 2023 at 06:53)
• @[coe] toFun (1 message, latest: Feb 14 2023 at 04:14)
• to_additive newline docstrings (1 message, latest: Feb 14 2023 at 00:53)
• Topology.Algebra.Monoid !4#2245 (5 messages, latest: Feb 14 2023 at 00:46)
• Default HSMul for !4#2212 (20 messages, latest: Feb 13 2023 at 23:04)
• coe_mk and similar lemmas (17 messages, latest: Feb 13 2023 at 22:27)
• @[continuity, to_additive] (11 messages, latest: Feb 13 2023 at 19:30)
• symmApply vs symm_apply (4 messages, latest: Feb 13 2023 at 17:35)
• formalizing growth of the Grigorchuk group in Lean 4 (19 messages, latest: Feb 13 2023 at 17:23)
• Depth-first search on quivers, with proof (13 messages, latest: Feb 13 2023 at 16:38)
• build 1 target (7 messages, latest: Feb 13 2023 at 16:13)
• Already-forward-ported files (26 messages, latest: Feb 13 2023 at 16:02)
• has_to_tactic_format (11 messages, latest: Feb 13 2023 at 15:34)
• CanLift !4#2256 (4 messages, latest: Feb 13 2023 at 14:41)
• restart port (10 messages, latest: Feb 13 2023 at 13:33)
• coercion from Nat to ENat (29 messages, latest: Feb 13 2023 at 08:08)
• LinearAlgebra.Basic !4#1979 (53 messages, latest: Feb 13 2023 at 06:07)
• Topology.Algebra.MulAction !4#2013 (9 messages, latest: Feb 13 2023 at 05:41)
• simps and semireducible (8 messages, latest: Feb 12 2023 at 22:31)
• In-Browser Lean 4 (5 messages, latest: Feb 12 2023 at 19:34)
• sorry { ... } trick in Lean4 (11 messages, latest: Feb 11 2023 at 23:44)
• ✔ nonrec vs root (80 messages, latest: Feb 11 2023 at 21:49)
• Typeclass resolution (20 messages, latest: Feb 11 2023 at 18:23)
• RingTheory.Subring.Basic !4#1945 (35 messages, latest: Feb 11 2023 at 16:37)
• Classes design and instances (8 messages, latest: Feb 11 2023 at 10:48)
• 2003 – review porting notes (1 message, latest: Feb 11 2023 at 09:05)
• MeasureTheory.PiSystem !4#2160 (6 messages, latest: Feb 11 2023 at 09:02)
• Data.List.Indexes !4#1812 (3 messages, latest: Feb 11 2023 at 08:18)
• Bundled morphisms (6 messages, latest: Feb 11 2023 at 07:40)
• Nonneg ring !4#1260 (13 messages, latest: Feb 11 2023 at 06:13)
• mathlib4#2122 (16 messages, latest: Feb 11 2023 at 01:59)
• documentation on the unit interval and metric spaces (1 message, latest: Feb 10 2023 at 23:08)
• bump to 2023-02-10 (34 messages, latest: Feb 10 2023 at 23:05)
• noncomputable (10 messages, latest: Feb 10 2023 at 20:46)
• HasContinuousSMul naming (9 messages, latest: Feb 10 2023 at 07:10)
• bump to 2023-02-06 (99 messages, latest: Feb 09 2023 at 19:52)
• reopen !4#1287 (19 messages, latest: Feb 09 2023 at 17:17)
• Data.Bitvec.Basic !4#2179 (8 messages, latest: Feb 09 2023 at 17:12)
• Bikeshedding: Data.Seq.Seq (16 messages, latest: Feb 09 2023 at 17:10)
• Classical (53 messages, latest: Feb 09 2023 at 16:17)
• lake exe cache curl version (12 messages, latest: Feb 09 2023 at 16:02)
• guard_hyp: can't guard this (14 messages, latest: Feb 09 2023 at 13:32)
• Pattern match against implicit arguments (6 messages, latest: Feb 09 2023 at 09:40)
• simp_rw not working as expected (1 message, latest: Feb 09 2023 at 07:39)
• @[trans] not building Transitive instance (2 messages, latest: Feb 08 2023 at 23:27)
• Addin @alexkassil on github for port (15 messages, latest: Feb 08 2023 at 19:35)
• Instances in !4#2138 (14 messages, latest: Feb 08 2023 at 17:27)
• stuck typeclass problem in try/catch (33 messages, latest: Feb 08 2023 at 15:45)
• ✔ Caching in CI (4 messages, latest: Feb 08 2023 at 14:48)
• SetTheory.Cardinal.Basic !4#2084 (1 message, latest: Feb 08 2023 at 11:20)
• Confusing "cases" behaviour (1 message, latest: Feb 08 2023 at 00:57)
• Bounded existential unexpander (8 messages, latest: Feb 07 2023 at 21:36)
• !4#2046 to_additive trouble (7 messages, latest: Feb 07 2023 at 20:05)
• convert failures (10 messages, latest: Feb 07 2023 at 19:53)
• GroupTheory.Divisible !4#2149 (6 messages, latest: Feb 07 2023 at 15:21)
• How to avoid the id-comp loop in aesop? (19 messages, latest: Feb 07 2023 at 11:48)
• .DS_Store in gitignore? (10 messages, latest: Feb 07 2023 at 05:43)
• Dangerous instances in !4#2127 (1 message, latest: Feb 07 2023 at 04:40)
• TagAttribute (22 messages, latest: Feb 07 2023 at 02:16)
• simpNF claims LHS doesn't simplify, but it does (18 messages, latest: Feb 06 2023 at 19:39)
• New dot lemmas (2 messages, latest: Feb 06 2023 at 17:11)
• notation/notation3 (7 messages, latest: Feb 06 2023 at 16:29)
• making a TacticM (27 messages, latest: Feb 06 2023 at 14:56)
• #lint in file is not an error (6 messages, latest: Feb 06 2023 at 13:20)
• !4#2084 wrong instances (6 messages, latest: Feb 06 2023 at 13:15)
• positivity with scientific notation (4 messages, latest: Feb 06 2023 at 09:35)
• lean4#2074 (new-style structures) (23 messages, latest: Feb 06 2023 at 06:49)
• ✔ Data.Multiset.Fintype 4!#1828 (17 messages, latest: Feb 06 2023 at 05:49)
• Bug in push_neg (7 messages, latest: Feb 06 2023 at 02:02)
• De Morgan Laws for booleans (18 messages, latest: Feb 05 2023 at 22:57)
• make tfae tactics a block tactic? (49 messages, latest: Feb 05 2023 at 22:51)
• mathport apply_rules (3 messages, latest: Feb 05 2023 at 22:42)
• polyrith debug output (2 messages, latest: Feb 05 2023 at 22:36)
• Data.PNat.Factors !4#1830 (4 messages, latest: Feb 05 2023 at 21:03)
• Algebra.Periodic !4#1963 (28 messages, latest: Feb 05 2023 at 19:58)
• NatCast (12 messages, latest: Feb 05 2023 at 17:08)
• Topology.ContinuousFunction.Basic (3 messages, latest: Feb 05 2023 at 14:24)
• to_additive, simps (14 messages, latest: Feb 05 2023 at 11:33)
• bInter and mathport (4 messages, latest: Feb 05 2023 at 11:26)
• delta; infer_instance (4 messages, latest: Feb 05 2023 at 10:29)
• linear_combination bug? (2 messages, latest: Feb 05 2023 at 09:30)
• simp_to_steps (4 messages, latest: Feb 05 2023 at 08:06)
• Lean 4 version of Exists.some? (2 messages, latest: Feb 05 2023 at 04:31)
• Approach for nthLe refactoring? (12 messages, latest: Feb 04 2023 at 23:22)
• lean bump (6 messages, latest: Feb 04 2023 at 18:42)
• naming bikeshed: ofFoo (21 messages, latest: Feb 04 2023 at 16:35)
• ✔ lake build builds independently of lean4 VS code exte… (34 messages, latest: Feb 04 2023 at 09:39)
• slow positivity (38 messages, latest: Feb 04 2023 at 07:33)
• apply incompatibility (4 messages, latest: Feb 03 2023 at 18:53)
• Combinatorics.Composition !4#2043 (2 messages, latest: Feb 03 2023 at 18:51)
• #1892 by exactI (9 messages, latest: Feb 03 2023 at 15:52)
• review meta code (1 message, latest: Feb 03 2023 at 13:05)
• olympiad problems with mathlib4 (36 messages, latest: Feb 03 2023 at 12:35)
• ext doesn't fire when it should (14 messages, latest: Feb 03 2023 at 09:46)
• mathlib3 in separate window (4 messages, latest: Feb 03 2023 at 09:16)
• apply doesn't like fun x => _ (60 messages, latest: Feb 03 2023 at 07:54)
• help-wanted label (11 messages, latest: Feb 03 2023 at 07:42)
• label after-port (16 messages, latest: Feb 03 2023 at 02:44)
• simpNF error behind simps (17 messages, latest: Feb 02 2023 at 20:59)
• Data.Fintype.Quotient !4#2019 (28 messages, latest: Feb 02 2023 at 19:20)
• bug in cases' goal management (9 messages, latest: Feb 02 2023 at 19:17)
• resolve projection notation (1 message, latest: Feb 02 2023 at 19:05)
• casesm changed behaviour !4#1744 (5 messages, latest: Feb 02 2023 at 17:14)
• Nat.sub =?= HSub.hSub (62 messages, latest: Feb 02 2023 at 09:05)
• calc blocks and heterogeneous operators (24 messages, latest: Feb 02 2023 at 04:22)
• noncomputable section breaks section end? (8 messages, latest: Feb 02 2023 at 02:06)
• issues at !4#1991 Data.Finsupp.AList (24 messages, latest: Feb 01 2023 at 20:31)
• mathport align issue? (10 messages, latest: Feb 01 2023 at 19:54)
• simp 1 <= x (14 messages, latest: Feb 01 2023 at 17:48)
• ✔ contextual simp variable subs (18 messages, latest: Feb 01 2023 at 16:12)
• Data.Set.Pointwise.Interval !4#1481 (2 messages, latest: Feb 01 2023 at 13:42)
• Citing mathlib4 & mathport (1 message, latest: Feb 01 2023 at 11:35)
• Data.Finset.Pointwise !4#1911 (3 messages, latest: Feb 01 2023 at 11:19)
• align bool,option,list,nat (2 messages, latest: Feb 01 2023 at 10:08)
• order on UpperSets (19 messages, latest: Feb 01 2023 at 09:32)
• fresh metavars (3 messages, latest: Feb 01 2023 at 09:15)
• use tactic is no longer finishing (9 messages, latest: Feb 01 2023 at 02:36)
• Data.Finsupp.Basic !4#1949 (3 messages, latest: Feb 01 2023 at 01:07)
• Finite set over infinite type (36 messages, latest: Jan 31 2023 at 22:23)
• deprecated lean3-ism convention (23 messages, latest: Jan 31 2023 at 21:39)
• ✔ Quote4 and tactics (8 messages, latest: Jan 31 2023 at 10:20)
• add missing #align statements !4#1966 (6 messages, latest: Jan 31 2023 at 09:29)
• Can't find instance (3 messages, latest: Jan 31 2023 at 08:00)
• finding simps lemmas (20 messages, latest: Jan 30 2023 at 23:55)
• open classical (8 messages, latest: Jan 30 2023 at 22:38)
• GroupTheory.Coset !4#1874 (3 messages, latest: Jan 30 2023 at 22:30)
• unknown free variable (36 messages, latest: Jan 30 2023 at 22:23)
• expected command, expected :=, expected structure (11 messages, latest: Jan 30 2023 at 20:12)
• notation overloading linter (1 message, latest: Jan 30 2023 at 19:32)
• to_additive for generated lemmas (18 messages, latest: Jan 30 2023 at 16:51)
• ✔ RingTheory.Subsemiring.Basic !4#1862 (5 messages, latest: Jan 30 2023 at 12:09)
• ✔ Algebra.GradedMulAction (4 messages, latest: Jan 30 2023 at 10:21)
• OfScientific (96 messages, latest: Jan 30 2023 at 06:36)
• obtain to massage syntactic equality (4 messages, latest: Jan 30 2023 at 06:06)
• simp priority (3 messages, latest: Jan 30 2023 at 04:59)
• RatCast ℚ instance (2 messages, latest: Jan 30 2023 at 02:59)
• linarith failure (23 messages, latest: Jan 29 2023 at 22:56)
• Singleton notation (9 messages, latest: Jan 29 2023 at 22:17)
• GroupTheory.GroupAction.SubMulAction.Pointwise (15 messages, latest: Jan 29 2023 at 15:48)
• removal of command line for teaching (15 messages, latest: Jan 29 2023 at 15:40)
• tagged releases? (39 messages, latest: Jan 29 2023 at 11:05)
• simplifying "dependent" match (1 message, latest: Jan 29 2023 at 07:11)
• add missing #align statements !4#1902 (4 messages, latest: Jan 29 2023 at 01:45)
• macro_rules with an argument (29 messages, latest: Jan 28 2023 at 22:17)
• data.analysis (8 messages, latest: Jan 28 2023 at 21:48)
• feat: port Algebra.BigOperators.Intervals (3 messages, latest: Jan 28 2023 at 19:18)
• tfae Tfae TFEA (13 messages, latest: Jan 28 2023 at 17:41)
• lake get-cache (652 messages, latest: Jan 28 2023 at 11:50)
• Lots of 1 + 1 + 1 + 1 (20 messages, latest: Jan 28 2023 at 05:35)
• another rat reducibility issue? (6 messages, latest: Jan 28 2023 at 02:46)
• Instance transparency issue? (28 messages, latest: Jan 28 2023 at 02:10)
• What is an outParam? (65 messages, latest: Jan 28 2023 at 01:21)
• unification weaker in lean4 (15 messages, latest: Jan 28 2023 at 01:13)
• coercion from PNat to Rat (5 messages, latest: Jan 27 2023 at 22:08)
• Rogue Int.ofNat maxing out recursion depth for decimals (8 messages, latest: Jan 27 2023 at 17:29)
• Combinatorics.SimpleGraph.Basic mathlib4#1883 (1 message, latest: Jan 27 2023 at 16:53)
• Data.Dfinsupp.Basic !4#1829 (17 messages, latest: Jan 27 2023 at 15:48)
• simpNF problems (10 messages, latest: Jan 27 2023 at 14:26)
• ✔ Group instance (6 messages, latest: Jan 27 2023 at 13:53)
• Data.Finsupp.Defs mathlib4#1807 (43 messages, latest: Jan 27 2023 at 12:57)
• reducible non-instances (2 messages, latest: Jan 27 2023 at 11:42)
• GroupTheory.GroupAction.ConjAct !4#1871 (6 messages, latest: Jan 27 2023 at 09:49)
• failed to synthesize Additive (Group G) (2 messages, latest: Jan 27 2023 at 03:36)
• DiscreteTopology bot (11 messages, latest: Jan 27 2023 at 02:13)
• simp under binders (16 messages, latest: Jan 26 2023 at 23:06)
• Diamond issue in Algebra.Star.Basic (9 messages, latest: Jan 26 2023 at 22:22)
• weird interaction between mod_cases and induction (12 messages, latest: Jan 26 2023 at 21:53)
• documented high level porting procedure in the wiki (2 messages, latest: Jan 26 2023 at 20:15)
• Algebra.Star.SelfAdjoint !4#1860 (1 message, latest: Jan 26 2023 at 19:05)
• Missing lemmas (9 messages, latest: Jan 26 2023 at 18:51)
• to_additive type mismatch (7 messages, latest: Jan 26 2023 at 17:13)
• Algebra.Module.Equiv mathlib4#1732 (44 messages, latest: Jan 26 2023 at 14:33)
• GroupTheory.Subgroup.Basic !4#1797 (12 messages, latest: Jan 26 2023 at 09:39)
• Order.Filter.Pointwise !4#1839 (1 message, latest: Jan 26 2023 at 04:29)
• Topology.Tactic (4 messages, latest: Jan 26 2023 at 00:17)
• unassigned metavariable in out-param (7 messages, latest: Jan 25 2023 at 21:45)
• Topology.Basic !4#1826 (11 messages, latest: Jan 25 2023 at 19:53)
• Topology.Bornology.Basic (13 messages, latest: Jan 25 2023 at 15:48)
• Order.LocallyFinite !4#1754 (12 messages, latest: Jan 25 2023 at 12:20)
• Order.Hom.Lattice (33 messages, latest: Jan 25 2023 at 12:09)
• mathlib4#1777 (1 message, latest: Jan 25 2023 at 07:58)
• ✔ epsilon (3 messages, latest: Jan 25 2023 at 06:06)
• to_additive with inductive (7 messages, latest: Jan 24 2023 at 22:00)
• Infer kinds are unsupported (10 messages, latest: Jan 24 2023 at 20:13)
• Algebra.Quandle held up by group (5 messages, latest: Jan 24 2023 at 19:43)
• attr := simp (17 messages, latest: Jan 24 2023 at 19:31)
• syntax matches when literal doesn't (4 messages, latest: Jan 24 2023 at 17:30)
• to_additive align failures (54 messages, latest: Jan 24 2023 at 16:55)
• conv (2 messages, latest: Jan 24 2023 at 13:54)
• data.bitvec.core mathlib4#1731 (10 messages, latest: Jan 24 2023 at 13:14)
• synport experimentation (105 messages, latest: Jan 24 2023 at 11:24)
• order.filter.germ (12 messages, latest: Jan 24 2023 at 11:08)
• decidable/classical (4 messages, latest: Jan 24 2023 at 09:13)
• ✔ port Data.LazyList.Basic (12 messages, latest: Jan 24 2023 at 08:15)
• linkifier (4 messages, latest: Jan 24 2023 at 08:06)
• Order.Filter.NAry (17 messages, latest: Jan 24 2023 at 05:19)
• order.filter.at_top_bot (3 messages, latest: Jan 24 2023 at 02:00)
• Data.Pfun Issues Summary ( mathlib4#1179) (2 messages, latest: Jan 23 2023 at 23:32)
• align private decls (20 messages, latest: Jan 23 2023 at 19:02)
• Set.mem_setOf_eq (7 messages, latest: Jan 23 2023 at 16:55)
• data.fin.vec_notation mathlib4#1741 (21 messages, latest: Jan 23 2023 at 16:45)
• [meta] avoiding multiple environments (6 messages, latest: Jan 23 2023 at 15:05)
• to_additive translating pow to nsmul (10 messages, latest: Jan 23 2023 at 13:44)
• elab_as_elim (5 messages, latest: Jan 23 2023 at 13:38)
• ✔ to_additive.map_namespace (7 messages, latest: Jan 23 2023 at 12:53)
• Remove a file from PR (24 messages, latest: Jan 23 2023 at 11:57)
• mathport issues (41 messages, latest: Jan 23 2023 at 09:42)
• linarith error in structured proof (8 messages, latest: Jan 23 2023 at 09:41)
• Union notation (2 messages, latest: Jan 23 2023 at 08:23)
• lift_pair etc (3 messages, latest: Jan 23 2023 at 08:22)
• linarith with discharger (8 messages, latest: Jan 23 2023 at 04:06)
• order.filter.basic (39 messages, latest: Jan 23 2023 at 02:48)
• nontriviality leaves metavars (6 messages, latest: Jan 22 2023 at 23:07)
• ring vs Ring (17 messages, latest: Jan 22 2023 at 20:46)
• induction, case, rcases (8 messages, latest: Jan 22 2023 at 18:54)
• Linter complains about porting note before docstring (3 messages, latest: Jan 22 2023 at 18:27)
• Port Order/OrderIsoNat (22 messages, latest: Jan 22 2023 at 17:18)
• Issues importing mathlib4 (57 messages, latest: Jan 22 2023 at 16:31)
• [field_simp] simp timeout (45 messages, latest: Jan 22 2023 at 08:56)
• default "/" meaning (22 messages, latest: Jan 21 2023 at 10:33)
• Data.Set.Finite mathlib4#1734 (47 messages, latest: Jan 21 2023 at 03:25)
• norm_num yielding 1/1 (1 message, latest: Jan 21 2023 at 03:08)
• congr tactic hitting max recursion depth (13 messages, latest: Jan 21 2023 at 01:02)
• my PRs that need help (22 messages, latest: Jan 21 2023 at 00:04)
• Logic.Equiv.Array (5 messages, latest: Jan 20 2023 at 23:11)
• [CI] error getting cache (51 messages, latest: Jan 20 2023 at 19:51)
• Data.Fintype.Vector mathlib4#1716 (42 messages, latest: Jan 20 2023 at 18:29)
• import name changes (1 message, latest: Jan 20 2023 at 16:41)
• Data.SetLike.Fintype mathlib4#1727 (6 messages, latest: Jan 20 2023 at 16:25)
• how to port? (35 messages, latest: Jan 20 2023 at 15:48)
• BigOperators parsing precedence (14 messages, latest: Jan 20 2023 at 15:21)
• algebra.module.linear_map mathlib4#1587 (8 messages, latest: Jan 20 2023 at 14:10)
• Data.Zmod.Defs mathlib4#1713 (3 messages, latest: Jan 20 2023 at 13:02)
• Data.Sym.Basic mathlib4#1672 (10 messages, latest: Jan 20 2023 at 09:21)
• norm_num characteristic functionality (55 messages, latest: Jan 20 2023 at 08:51)
• Data.Nat.Factors mathlib4#1664 (8 messages, latest: Jan 20 2023 at 04:58)
• New solve_by_elim (43 messages, latest: Jan 20 2023 at 01:06)
• enat (19 messages, latest: Jan 19 2023 at 23:31)
• Instance naming for Equiv instances (2 messages, latest: Jan 19 2023 at 21:13)
• Potential Bug in symm tactic (23 messages, latest: Jan 19 2023 at 19:58)
• starting the port of a new file (68 messages, latest: Jan 19 2023 at 19:09)
• strange type issue in mathlib4#1685 (5 messages, latest: Jan 19 2023 at 19:02)
• Invalid auto and opt values (1 message, latest: Jan 19 2023 at 17:24)
• unusedArguments (1 message, latest: Jan 19 2023 at 16:53)
• data.nat.fib mathlib4#1644 (63 messages, latest: Jan 19 2023 at 15:39)
• Linter complains about let rec missing docstring (9 messages, latest: Jan 19 2023 at 14:59)
• Hypothesis renaming — mathlib4#1658 (12 messages, latest: Jan 19 2023 at 14:13)
• zify bugs? (6 messages, latest: Jan 19 2023 at 12:38)
• Updating SHAs for modified files (7 messages, latest: Jan 19 2023 at 12:25)
• finset.sum_smul (3 messages, latest: Jan 19 2023 at 11:43)
• Data.Finset.Sups mathlib4#1663 (14 messages, latest: Jan 19 2023 at 10:41)
• Data.Fin.Tuple.Basic mathlib4#1516 (35 messages, latest: Jan 19 2023 at 09:10)
• change … with replacement (2 messages, latest: Jan 18 2023 at 20:10)
• generalized functions of Fin n? (17 messages, latest: Jan 18 2023 at 19:36)
• help wanted porting Algebra.Order.Module (3 messages, latest: Jan 18 2023 at 19:03)
• setOf unexpander (7 messages, latest: Jan 18 2023 at 16:26)
• Prop -> Bool regression (52 messages, latest: Jan 18 2023 at 15:41)
• Computable Fin Induction (7 messages, latest: Jan 18 2023 at 14:52)
• open_locale big_operators (6 messages, latest: Jan 18 2023 at 14:38)
• Algebra.BigOperators.Basic mathlib4#1628 (16 messages, latest: Jan 18 2023 at 13:20)
• indentation, by (10 messages, latest: Jan 18 2023 at 11:26)
• Meaning of specialize (9 messages, latest: Jan 18 2023 at 09:45)
• mathlib3port not updating (11 messages, latest: Jan 18 2023 at 08:58)
• Using List.get in Vector.Basic (27 messages, latest: Jan 18 2023 at 07:42)
• data.finmap mathlib4#1591 (26 messages, latest: Jan 18 2023 at 01:38)
• matching a non-merged mathlib3 PR (3 messages, latest: Jan 18 2023 at 00:25)
• recursive ext in Lean 4? (8 messages, latest: Jan 17 2023 at 23:21)
• Order.OmegaCompletePartialOrder mathlib4#1168 (7 messages, latest: Jan 17 2023 at 19:04)
• data.finset.lattice mathlib4#1606 (17 messages, latest: Jan 17 2023 at 16:30)
• What does "unexpected syntax" mean? (6 messages, latest: Jan 17 2023 at 15:11)
• Order.SupIndep mathlib4#1627 (6 messages, latest: Jan 17 2023 at 14:29)
• Abelian categories (4 messages, latest: Jan 17 2023 at 12:47)
• Can't SmulCommClass.symm be an instance? (6 messages, latest: Jan 17 2023 at 11:44)
• data.real.basic mathlib4#1514 (44 messages, latest: Jan 17 2023 at 08:59)
• Help with Universe Levels (18 messages, latest: Jan 17 2023 at 03:29)
• Transparency setting in solve_by_elim (9 messages, latest: Jan 17 2023 at 01:48)
• Finset.Prod: ambigiuous notation (6 messages, latest: Jan 16 2023 at 21:10)
• #1594 Order.Grade (2 messages, latest: Jan 16 2023 at 17:34)
• Definition of subset (20 messages, latest: Jan 16 2023 at 11:18)
• list.repeat (30 messages, latest: Jan 16 2023 at 10:48)
• Algebra.Hom.GroupAction mathlib4#1424 (2 messages, latest: Jan 16 2023 at 10:45)
• Sep notation (6 messages, latest: Jan 16 2023 at 10:15)
• Int division, again (1 message, latest: Jan 16 2023 at 10:10)
• How to import a file in test/ in another file in test/? (2 messages, latest: Jan 16 2023 at 09:12)
• List (2 messages, latest: Jan 16 2023 at 09:08)
• Data.Finset.Basic mathlib4#1555 (37 messages, latest: Jan 16 2023 at 08:03)
• IsTrans (33 messages, latest: Jan 15 2023 at 21:16)
• Algebra.Free (8 messages, latest: Jan 15 2023 at 16:22)
• BEq DecidableEq Diamond (22 messages, latest: Jan 15 2023 at 06:37)
• Notes on Ordmap.Ordnode (8 messages, latest: Jan 15 2023 at 04:04)
• what's the n argument for Repr.reprPrec? (3 messages, latest: Jan 15 2023 at 00:37)
• Correct formulation of induction principles (24 messages, latest: Jan 15 2023 at 00:00)
• Rat in norm_num (97 messages, latest: Jan 14 2023 at 22:32)
• Question about implicit coercions and the linter (8 messages, latest: Jan 14 2023 at 22:07)
• ✔ false alarm about norm_num (11 messages, latest: Jan 14 2023 at 21:14)
• Randomness (89 messages, latest: Jan 14 2023 at 20:00)
• rw not working as expected (9 messages, latest: Jan 14 2023 at 17:42)
• Algebra.Hom.GroupAction (19 messages, latest: Jan 14 2023 at 14:28)
• Mathport $ -> <\| (11 messages, latest: Jan 14 2023 at 13:48)
• docs4 broken (5 messages, latest: Jan 14 2023 at 13:39)
• simpNF definition of "simplified"? (25 messages, latest: Jan 14 2023 at 10:37)
• semi/irreducible attributes (14 messages, latest: Jan 14 2023 at 09:41)
• unexpected eliminator resulting type (6 messages, latest: Jan 14 2023 at 08:42)
• Some Smuls in code (3 messages, latest: Jan 14 2023 at 06:58)
• Similar theorems in different files with same name (5 messages, latest: Jan 14 2023 at 05:49)
• defLemma failing when it seems it shouldn't (5 messages, latest: Jan 14 2023 at 04:59)
• casesm / constructorm on no match: error or not? (10 messages, latest: Jan 13 2023 at 23:48)
• "help wanted" (3 messages, latest: Jan 13 2023 at 23:23)
• mathport import naming (2 messages, latest: Jan 13 2023 at 22:06)
• Possible to remove rename_i here? (2 messages, latest: Jan 13 2023 at 21:17)
• Test for dsimp vs simp with simp lint? (12 messages, latest: Jan 13 2023 at 19:50)
• docs4#Rat.den_nz (1 message, latest: Jan 13 2023 at 18:08)
• Data.Set.Semiring (21 messages, latest: Jan 13 2023 at 16:49)
• data.int.succ_pred (3 messages, latest: Jan 13 2023 at 15:38)
• simpNF (5 messages, latest: Jan 13 2023 at 15:36)
• trans attribute (19 messages, latest: Jan 13 2023 at 14:57)
• Order.Hom.Bounded mathlib4#888 (2 messages, latest: Jan 13 2023 at 14:37)
• tt/ff (6 messages, latest: Jan 13 2023 at 14:33)
• updating names in VSCode (3 messages, latest: Jan 13 2023 at 13:30)
• structured CLI apps (1 message, latest: Jan 13 2023 at 11:50)
• general JSON to lean4 support (7 messages, latest: Jan 13 2023 at 11:15)
• Data.Multiset.Basic mathlib4#1491 (64 messages, latest: Jan 13 2023 at 09:39)
• Eq.recOn (8 messages, latest: Jan 13 2023 at 08:55)
• Data.List.Sublists mathlib4#1494 (16 messages, latest: Jan 13 2023 at 08:37)
• Data.Fin.Basic (mathlib4#1084) (255 messages, latest: Jan 13 2023 at 06:56)
• print instances (1 message, latest: Jan 13 2023 at 03:49)
• moving Data.List.Perm to std (1 message, latest: Jan 12 2023 at 23:41)
• split syntax (2 messages, latest: Jan 12 2023 at 23:08)
• norm_cast bug (9 messages, latest: Jan 12 2023 at 22:17)
• SetTheory.Game.Pgame (3 messages, latest: Jan 12 2023 at 21:54)
• interval_oc naming scheme (10 messages, latest: Jan 12 2023 at 21:03)
• Order.Circular mathlib4#1489 (38 messages, latest: Jan 12 2023 at 18:45)
• #align (16 messages, latest: Jan 12 2023 at 18:37)
• Data.List.Sublists (1 message, latest: Jan 12 2023 at 17:53)
• to_additive can't map multiplicative ℕ to ℕ (5 messages, latest: Jan 12 2023 at 11:57)
• Heterogeneous scalar multiplication (26 messages, latest: Jan 12 2023 at 11:29)
• application type mismatch error (2 messages, latest: Jan 12 2023 at 09:44)
• help wanted porting Algebra.Hom.Centroid (16 messages, latest: Jan 12 2023 at 08:32)
• port Data.Set.Intervals.Instances (7 messages, latest: Jan 12 2023 at 08:10)
• elaborate eliminator (2 messages, latest: Jan 12 2023 at 07:10)
• Data.List.Rotate mathlib#1490 (3 messages, latest: Jan 12 2023 at 04:32)
• Invertible 1 simps (37 messages, latest: Jan 12 2023 at 02:23)
• Parsing error (7 messages, latest: Jan 12 2023 at 00:41)
• List.Mem as Or? (3 messages, latest: Jan 11 2023 at 20:30)
• Universes issue in mathlib#1464 (3 messages, latest: Jan 11 2023 at 20:18)
• mathport runs (20 messages, latest: Jan 11 2023 at 19:42)
• Data.List.Perm mathlib4#1478 (19 messages, latest: Jan 11 2023 at 16:35)
• List.union (50 messages, latest: Jan 11 2023 at 13:23)
• Data.List.Intervals mathlib4#1479 (1 message, latest: Jan 11 2023 at 08:01)
• Data.List.Perm (6 messages, latest: Jan 11 2023 at 04:45)
• typeclass instance problem with singleton (15 messages, latest: Jan 11 2023 at 03:52)
• apply function to hypothesis (9 messages, latest: Jan 11 2023 at 02:47)
• premature "goals accomplished" (92 messages, latest: Jan 11 2023 at 00:46)
• rw failing to rewrite coercions…but only sometimes (27 messages, latest: Jan 10 2023 at 20:59)
• Data.List.Range mathlib4#1463 (3 messages, latest: Jan 10 2023 at 20:47)
• ext (34 messages, latest: Jan 10 2023 at 19:59)
• What's the general fix for Lean too eagerly unfolding (1 message, latest: Jan 10 2023 at 18:58)
• Data.List.Nodup (mathlib4#1456) (2 messages, latest: Jan 10 2023 at 17:27)
• Data.Set.Pointwise.Basic (mathlib4#1188) (8 messages, latest: Jan 10 2023 at 16:33)
• rewrite tactic reaching maximum heartbeat (3 messages, latest: Jan 10 2023 at 15:42)
• renaming in mathport (1 message, latest: Jan 10 2023 at 13:36)
• Control.Traversable.Instances (mathlib4#1393) (1 message, latest: Jan 10 2023 at 12:03)
• Data.List.Count (mathlib4#1410) (11 messages, latest: Jan 10 2023 at 12:01)
• mathport funext (19 messages, latest: Jan 10 2023 at 10:09)
• Data.List.Func (15 messages, latest: Jan 10 2023 at 09:45)
• coe type linter (1 message, latest: Jan 10 2023 at 07:10)
• Get-cache (57 messages, latest: Jan 10 2023 at 06:00)
• local attribute [- …] (125 messages, latest: Jan 09 2023 at 21:40)
• dangerous instances (2 messages, latest: Jan 09 2023 at 20:50)
• Data.List.BigOperators.Basic mathlib4#1380 (12 messages, latest: Jan 09 2023 at 19:19)
• improved interaction of to_additive with other attributes (4 messages, latest: Jan 09 2023 at 18:38)
• Identity map of Natural Numbers is strictly monotone (3 messages, latest: Jan 09 2023 at 08:49)
• rename Nat.le_or_eq_or_le_succ (2 messages, latest: Jan 09 2023 at 04:46)
• Rat.floor (6 messages, latest: Jan 08 2023 at 17:44)
• norm_cast (15 messages, latest: Jan 08 2023 at 17:41)
• rfl (4 messages, latest: Jan 08 2023 at 13:33)
• Nat.mod 0 n = 0 no longer true by rfl (32 messages, latest: Jan 08 2023 at 12:14)
• data.nat.bitwise (57 messages, latest: Jan 08 2023 at 03:37)
• Linarith with nats (10 messages, latest: Jan 07 2023 at 23:50)
• simp experts: priority for commutatitve case? (20 messages, latest: Jan 07 2023 at 20:42)
• spelling Bool-valued operations (12 messages, latest: Jan 07 2023 at 18:01)
• map_natCast (3 messages, latest: Jan 07 2023 at 17:11)
• Functor id / Seq id (4 messages, latest: Jan 07 2023 at 17:02)
• Proving if rhs is some a lhs must be some (21 messages, latest: Jan 07 2023 at 09:43)
• ✔ simp normal form (1 message, latest: Jan 07 2023 at 08:45)
• Writing tests that fail (22 messages, latest: Jan 07 2023 at 08:01)
• SimpNF failing to suggest right simp (2 messages, latest: Jan 07 2023 at 07:52)
• source header (19 messages, latest: Jan 07 2023 at 05:09)
• Try this (6 messages, latest: Jan 07 2023 at 04:18)
• Interaction of abel with casting (12 messages, latest: Jan 07 2023 at 03:18)
• naming: map_int_cast vs map_natCast vs map_ratCast (18 messages, latest: Jan 07 2023 at 03:13)
• Data.Real.CauSeq (mathlib4#1124) (12 messages, latest: Jan 07 2023 at 03:12)
• Non-local behaviour in abel (24 messages, latest: Jan 07 2023 at 01:00)
• Importing Data.String.Basic (25 messages, latest: Jan 07 2023 at 00:41)
• lake update (8 messages, latest: Jan 06 2023 at 18:47)
• to_isSomePropStructure (7 messages, latest: Jan 06 2023 at 17:45)
• docs4#Int.ofNat_le (3 messages, latest: Jan 06 2023 at 14:46)
• # The following files have been modified since … (42 messages, latest: Jan 06 2023 at 14:41)
• Mass edit tools (8 messages, latest: Jan 06 2023 at 12:37)
• Merging mathlib3 PRs before creating forward-ports (25 messages, latest: Jan 06 2023 at 10:21)
• Last sorries in mathlib4 (16 messages, latest: Jan 06 2023 at 09:51)
• resetI (9 messages, latest: Jan 06 2023 at 09:13)
• deprecated.group (13 messages, latest: Jan 06 2023 at 07:57)
• toDual/ofDual alignment (5 messages, latest: Jan 06 2023 at 05:44)
• mfld_set_tac broken (5 messages, latest: Jan 06 2023 at 05:31)
• ✔ linarith failure (2 messages, latest: Jan 06 2023 at 01:34)
• Issue porting Algebra.Hom.Centroid.coe_to_add_monoid_hom… (13 messages, latest: Jan 06 2023 at 00:08)
• typeclass instance that fails linting (13 messages, latest: Jan 05 2023 at 23:50)
• Porting Nat.mod_def (11 messages, latest: Jan 05 2023 at 23:48)
• see commits in deleted branch? (15 messages, latest: Jan 05 2023 at 22:42)
• porting requests (117 messages, latest: Jan 05 2023 at 22:26)
• Data.Fin.Basic (41 messages, latest: Jan 05 2023 at 22:02)
• Data.List.Basic (223 messages, latest: Jan 05 2023 at 21:57)
• Monad List (12 messages, latest: Jan 05 2023 at 19:54)
• ambiguous interpretation at Data.List.Infix (15 messages, latest: Jan 05 2023 at 19:47)
• unsafe def (5 messages, latest: Jan 05 2023 at 18:53)
• simp can prove it (46 messages, latest: Jan 05 2023 at 17:53)
• New PRs (125 messages, latest: Jan 05 2023 at 16:56)
• Coercion to function dificulty (28 messages, latest: Jan 05 2023 at 14:45)
• simp? drops ← (1 message, latest: Jan 05 2023 at 14:23)
• pinned dependencies (19 messages, latest: Jan 05 2023 at 13:48)
• docs4#Set.BijOn (3 messages, latest: Jan 05 2023 at 12:28)
• docs#int.nat_mod (18 messages, latest: Jan 05 2023 at 11:56)
• merging or squash merging? (10 messages, latest: Jan 05 2023 at 10:26)
• simp? trace (1 message, latest: Jan 05 2023 at 09:32)
• simp normal form (52 messages, latest: Jan 04 2023 at 22:29)
• problems installing lean4/mathlib4 (1 message, latest: Jan 04 2023 at 20:43)
• strange error in to_additive (5 messages, latest: Jan 04 2023 at 17:29)
• port_status not picking up a PR (15 messages, latest: Jan 04 2023 at 09:30)
• Scoped attribute (10 messages, latest: Jan 04 2023 at 07:46)
• mathport and forward-porting (21 messages, latest: Jan 04 2023 at 01:56)
• ✔ How does one avoid rename_i here? (4 messages, latest: Jan 04 2023 at 01:55)
• How does one avoid rename_i here? (1 message, latest: Jan 04 2023 at 01:28)
• mathport lag (9 messages, latest: Jan 04 2023 at 00:59)
• syntax/macro question (5 messages, latest: Jan 03 2023 at 19:22)
• elab_strategy (13 messages, latest: Jan 03 2023 at 17:19)
• ✔ some_spec (4 messages, latest: Jan 03 2023 at 10:48)
• Nat.lt_add_left (2 messages, latest: Jan 03 2023 at 10:38)
• dependent PRs (21 messages, latest: Jan 03 2023 at 10:05)
• mathlib4 dark theme (2 messages, latest: Jan 03 2023 at 08:38)
• ✔ coe and norm_cast (7 messages, latest: Jan 02 2023 at 21:45)
• Performance issue with CompleteBooleanAlgebra (57 messages, latest: Jan 02 2023 at 20:58)
• synchronization label bot (28 messages, latest: Jan 02 2023 at 20:51)
• Exists elaboration and bUnion (17 messages, latest: Jan 02 2023 at 19:50)
• Kleisli(Cat) (15 messages, latest: Jan 02 2023 at 18:05)
• Order.SuccPred.Relation (5 messages, latest: Jan 02 2023 at 13:51)
• porting Data.Nat.WithBot (8 messages, latest: Jan 02 2023 at 12:44)
• unknown attributes (11 messages, latest: Jan 02 2023 at 08:16)
• Data.Int.Bitwise mathlib4#1159 (2 messages, latest: Jan 02 2023 at 07:53)
• Bug in rcases? (2 messages, latest: Jan 02 2023 at 05:29)
• (2 : ℕ+) (16 messages, latest: Jan 01 2023 at 23:47)
• obviously replacement in category theory (6 messages, latest: Jan 01 2023 at 23:36)
• Local notation conflict (9 messages, latest: Jan 01 2023 at 20:51)
• export (1 message, latest: Jan 01 2023 at 19:21)
• nat.bit / nat.binary_rec (21 messages, latest: Jan 01 2023 at 18:37)
• version incompatibilities (4 messages, latest: Dec 31 2022 at 21:18)
• Modeq name (74 messages, latest: Dec 31 2022 at 15:21)
• data.rat.cast mathlib4#1261 (3 messages, latest: Dec 31 2022 at 04:54)
• complete partial order formalization (9 messages, latest: Dec 30 2022 at 13:18)
• mathport simps translation (1 message, latest: Dec 29 2022 at 11:16)
• #queue4 (9 messages, latest: Dec 29 2022 at 11:10)
• algebra.euclidean_domain.instances (6 messages, latest: Dec 28 2022 at 19:47)
• (deleted) (1 message, latest: Dec 28 2022 at 18:46)
• Docs navigation (6 messages, latest: Dec 27 2022 at 21:00)
• Name check (5 messages, latest: Dec 27 2022 at 20:17)
• Subtype.mono_coe (2 messages, latest: Dec 27 2022 at 18:36)
• How to spell coe in Lean4 (4 messages, latest: Dec 27 2022 at 16:56)
• by exact (1 message, latest: Dec 27 2022 at 13:53)
• ordcontinuous (8 messages, latest: Dec 27 2022 at 11:25)
• typeclass loops (4 messages, latest: Dec 27 2022 at 00:12)
• SimpNF issues in PNat.find (5 messages, latest: Dec 26 2022 at 21:35)
• TC synthesis timeout (9 messages, latest: Dec 26 2022 at 19:58)
• Data.Real.CauSeq (107 messages, latest: Dec 26 2022 at 16:36)
• pretty printing Equiv (17 messages, latest: Dec 26 2022 at 11:21)
• [mathlib/test/.lean](topic/mathlib.2Ftest.2F.2Elean.html) (3 messages, latest: Dec 25 2022 at 20:47)
• Name for ZFC Set (12 messages, latest: Dec 25 2022 at 19:50)
• <| (20 messages, latest: Dec 25 2022 at 17:55)
• More issues with normalization to pp'able equalities (3 messages, latest: Dec 24 2022 at 19:16)
• ci on master is failing (2 messages, latest: Dec 24 2022 at 19:05)
• simp discharging (5 messages, latest: Dec 24 2022 at 17:07)
• Mathlib.Order.Copy (8 messages, latest: Dec 24 2022 at 15:35)
• attribute [local simp] (5 messages, latest: Dec 24 2022 at 13:31)
• ₓ (6 messages, latest: Dec 24 2022 at 13:03)
• #align to_additive (3 messages, latest: Dec 24 2022 at 11:08)
• alias & #align (1 message, latest: Dec 24 2022 at 10:06)
• git error from port_status on macOS (43 messages, latest: Dec 24 2022 at 00:17)
• Data.Int.Associated (3 messages, latest: Dec 24 2022 at 00:03)
• Control.Fix (2 messages, latest: Dec 23 2022 at 23:17)
• Data.Set.Pairwise (40 messages, latest: Dec 23 2022 at 19:41)
• Docs not updated (44 messages, latest: Dec 23 2022 at 19:03)
• Mathlib.Order.ConditionallyCompleteLattice.Basic (21 messages, latest: Dec 23 2022 at 18:07)
• LawfulMonad (4 messages, latest: Dec 23 2022 at 17:22)
• Data.Rat.Lemmas mathlib4#1138 (1 message, latest: Dec 23 2022 at 13:55)
• Classical.choose (2 messages, latest: Dec 23 2022 at 06:53)
• lift (6 messages, latest: Dec 22 2022 at 22:02)
• rcases (36 messages, latest: Dec 22 2022 at 21:09)
• use (51 messages, latest: Dec 22 2022 at 20:16)
• Data.Nat.EvenOddRec (99 messages, latest: Dec 22 2022 at 19:59)
• data.nat.prime #1156 (18 messages, latest: Dec 22 2022 at 16:49)
• local linting in porting wiki? (3 messages, latest: Dec 22 2022 at 14:30)
• pow_succ (8 messages, latest: Dec 22 2022 at 14:02)
• Order.Hom.Order mathlib4#1152 (4 messages, latest: Dec 22 2022 at 12:16)
• deriving instances (5 messages, latest: Dec 22 2022 at 08:34)
• div notation and rfl (13 messages, latest: Dec 22 2022 at 01:21)
• square roots are square roots (35 messages, latest: Dec 22 2022 at 00:41)
• Lean not "seeing through" composition (29 messages, latest: Dec 22 2022 at 00:08)
• dsimp before rw (24 messages, latest: Dec 21 2022 at 23:25)
• simp only [foo] not working but simp [foo] works (9 messages, latest: Dec 21 2022 at 20:26)
• naming convention check (2 messages, latest: Dec 21 2022 at 19:46)
• Data.Set.Lattice (13 messages, latest: Dec 21 2022 at 19:33)
• Algebra.Ring.Pi (12 messages, latest: Dec 21 2022 at 18:30)
• Algebra.Ring.Equiv help request (23 messages, latest: Dec 21 2022 at 17:58)
• complete_lattice and has_sup (43 messages, latest: Dec 21 2022 at 15:42)
• mathport ∀ a b c ∈ s (13 messages, latest: Dec 21 2022 at 13:41)
• mathlib4#1129 (39 messages, latest: Dec 21 2022 at 02:16)
• data.nat.bits (148 messages, latest: Dec 20 2022 at 22:39)
• Data.Int.Gcd - NormNum (9 messages, latest: Dec 20 2022 at 17:36)
• ✔ porting autoparams with identifiers (2 messages, latest: Dec 20 2022 at 17:35)
• diffing porting PR against initial commit (11 messages, latest: Dec 20 2022 at 15:39)
• port status (59 messages, latest: Dec 20 2022 at 13:59)
• CategoryTheory.Functor.FullyFaithful (62 messages, latest: Dec 20 2022 at 08:55)
• Data.Rat.Defs (128 messages, latest: Dec 20 2022 at 02:03)
• to_additive interaction with reducible (3 messages, latest: Dec 20 2022 at 00:06)
• Why is coe_mk no longer needed? (8 messages, latest: Dec 19 2022 at 23:57)
• porting autoparams with identifiers (1 message, latest: Dec 19 2022 at 22:46)
• mathlib4-port-status-new (12 messages, latest: Dec 19 2022 at 21:54)
• Set.compl and HasCompl.compl (5 messages, latest: Dec 19 2022 at 20:01)
• leanproject port command (18 messages, latest: Dec 19 2022 at 19:15)
• refine_struct alternative? (5 messages, latest: Dec 19 2022 at 18:15)
• Order.GaloisConnection (43 messages, latest: Dec 19 2022 at 16:48)
• Naming clarification (92 messages, latest: Dec 19 2022 at 16:08)
• Alignment not firing (7 messages, latest: Dec 19 2022 at 12:53)
• import Lean (5 messages, latest: Dec 19 2022 at 10:34)
• Algebra.GroupPower.Lemmas (40 messages, latest: Dec 19 2022 at 10:11)
• make MulOpposite a structure (15 messages, latest: Dec 18 2022 at 22:47)
• where did the noisy linter go? (7 messages, latest: Dec 18 2022 at 20:07)
• HasInvolutiveReverse / HasReverse (1 message, latest: Dec 18 2022 at 10:14)
• What is 2? (8 messages, latest: Dec 18 2022 at 10:02)
• Pi.Single misnomer (6 messages, latest: Dec 17 2022 at 22:45)
• ✔ Porting long strings after to_additive? (6 messages, latest: Dec 17 2022 at 21:26)
• Porting long strings after to_additive? (1 message, latest: Dec 17 2022 at 21:02)
• doc blame linter and prop (4 messages, latest: Dec 17 2022 at 18:50)
• notation3 (31 messages, latest: Dec 17 2022 at 18:48)
• to_additive questions and issues (64 messages, latest: Dec 17 2022 at 11:09)
• Problems with variables being unused (4 messages, latest: Dec 17 2022 at 06:51)
• Dealing with HMul (etc.)? (3 messages, latest: Dec 17 2022 at 00:45)
• not porting pi_instance (14 messages, latest: Dec 16 2022 at 22:57)
• unexpected variables (10 messages, latest: Dec 16 2022 at 21:46)
• Int.coe_natAbs misnomer (19 messages, latest: Dec 16 2022 at 17:40)
• data.set.intervals.basic (23 messages, latest: Dec 16 2022 at 16:13)
• Online docs (17 messages, latest: Dec 16 2022 at 11:49)
• scoped[NS] (25 messages, latest: Dec 16 2022 at 08:11)
• Nasty order of arguments dependency for @[refl] (7 messages, latest: Dec 15 2022 at 23:55)
• Order.Bounded mathlib4#1042 (3 messages, latest: Dec 15 2022 at 21:24)
• bors batch info (2 messages, latest: Dec 15 2022 at 19:37)
• alias unfolds definitions (8 messages, latest: Dec 15 2022 at 17:56)
• Logic.Equiv.Set (2 messages, latest: Dec 15 2022 at 17:14)
• Algebra.Group.Opposite (18 messages, latest: Dec 15 2022 at 16:27)
• Algebra.GroupPower.Order (16 messages, latest: Dec 15 2022 at 13:34)
• Difference in simp behaviour (62 messages, latest: Dec 15 2022 at 11:08)
• Data.Set.Enumerate (8 messages, latest: Dec 15 2022 at 09:21)
• data.set.function (25 messages, latest: Dec 15 2022 at 08:36)
• source references (1 message, latest: Dec 15 2022 at 08:09)
• cases assumption name (4 messages, latest: Dec 15 2022 at 03:01)
• CI: Cancelling outdated builds (5 messages, latest: Dec 15 2022 at 02:37)
• ✔ error building mathlib4 (6 messages, latest: Dec 15 2022 at 00:41)
• ✔ use prebuilt release? (4 messages, latest: Dec 14 2022 at 23:57)
• merging (9 messages, latest: Dec 14 2022 at 23:47)
• fixing library_note references (5 messages, latest: Dec 14 2022 at 20:55)
• unique term inhabiting the unit (13 messages, latest: Dec 14 2022 at 20:13)
• unfold working differently in Lean 4 (4 messages, latest: Dec 14 2022 at 19:59)
• #1001 failed to synthesize instance (7 messages, latest: Dec 14 2022 at 18:11)
• Heuristics for "typeclass instance problem"? (2 messages, latest: Dec 14 2022 at 17:37)
• simpNF and MulOpposite (3 messages, latest: Dec 14 2022 at 17:24)
• mathport issues in data.int.least_greatest (15 messages, latest: Dec 14 2022 at 16:54)
• existential binding (9 messages, latest: Dec 14 2022 at 10:41)
• Data.Part (5 messages, latest: Dec 14 2022 at 09:30)
• data.int.gcd (9 messages, latest: Dec 14 2022 at 09:07)
• Data.Int.Order.Basic (23 messages, latest: Dec 14 2022 at 08:09)
• simp regression with MonoidHomClass (11 messages, latest: Dec 14 2022 at 00:56)
• #align when mathport has it right (9 messages, latest: Dec 13 2022 at 23:34)
• ✔ using mathlib4 tactics in porting? (4 messages, latest: Dec 13 2022 at 23:14)
• assert_not_exists (1 message, latest: Dec 13 2022 at 21:40)
• bool.tt (9 messages, latest: Dec 13 2022 at 18:14)
• ✔ split fails but constructor works. (3 messages, latest: Dec 13 2022 at 18:02)
• split fails but constructor works. (5 messages, latest: Dec 13 2022 at 16:15)
• referring to namespace in theorem name (3 messages, latest: Dec 13 2022 at 16:13)
• indentation issue in mathport (2 messages, latest: Dec 13 2022 at 14:18)
• implicit argument in mathlibport field (5 messages, latest: Dec 13 2022 at 13:56)
• Int.ofNat and Nat.Cast (36 messages, latest: Dec 13 2022 at 11:43)
• Structure inheritance (2 messages, latest: Dec 12 2022 at 15:10)
• @[simps] making lemmas not in simp normal form (14 messages, latest: Dec 12 2022 at 10:32)
• Type synonyms (81 messages, latest: Dec 12 2022 at 09:59)
• div_def (4 messages, latest: Dec 12 2022 at 08:36)
• data.set.image (6 messages, latest: Dec 12 2022 at 07:12)
• data.set.basic (164 messages, latest: Dec 12 2022 at 06:51)
• Exists and simp_rw (5 messages, latest: Dec 11 2022 at 23:24)
• to_additive failure (9 messages, latest: Dec 11 2022 at 19:21)
• #align and simps (3 messages, latest: Dec 11 2022 at 19:12)
• Porting category theory (28 messages, latest: Dec 10 2022 at 17:18)
• #port-status not showing modified files (52 messages, latest: Dec 09 2022 at 19:23)
• Emitting warnings in mathlib3 CI (8 messages, latest: Dec 09 2022 at 18:59)
• set image notation (34 messages, latest: Dec 09 2022 at 14:22)
• simp (or refl?) difference Lean 3/4 (33 messages, latest: Dec 09 2022 at 13:58)
• Difference in simp lemma priorities? (11 messages, latest: Dec 09 2022 at 13:56)
• simp failing on partial application of projections (7 messages, latest: Dec 09 2022 at 12:21)
• simp calls broken in mathlib4#922 (17 messages, latest: Dec 09 2022 at 12:21)
• add_pow (5 messages, latest: Dec 09 2022 at 08:47)
• local semireducible (12 messages, latest: Dec 09 2022 at 04:03)
• expected '}' error from mathport (10 messages, latest: Dec 08 2022 at 22:33)
• request for help (7 messages, latest: Dec 08 2022 at 20:30)
• OfNat (60 messages, latest: Dec 08 2022 at 18:37)
• topology.algebra.order.basic (11 messages, latest: Dec 08 2022 at 15:43)
• elaboration failure in algebra.order.group.units (3 messages, latest: Dec 08 2022 at 12:07)
• Relying on instance names (27 messages, latest: Dec 08 2022 at 07:59)
• mathport #print (18 messages, latest: Dec 07 2022 at 22:54)
• #align and to_additive (12 messages, latest: Dec 07 2022 at 02:15)
• data.typevec (7 messages, latest: Dec 06 2022 at 23:36)
• coe_fn vs CoeFun (3 messages, latest: Dec 06 2022 at 22:57)
• unusedHavesSuffices false positive (7 messages, latest: Dec 06 2022 at 22:38)
• ✔ algebra.order.group.defs mathlib4#869 (2 messages, latest: Dec 06 2022 at 22:05)
• when does mathlib3port run / running it myself (6 messages, latest: Dec 06 2022 at 22:04)
• Naming smul vs sMul (7 messages, latest: Dec 06 2022 at 21:49)
• WriterT type variation on port (7 messages, latest: Dec 06 2022 at 18:38)
• algebra.order.group.defs mathlib4#869 (2 messages, latest: Dec 06 2022 at 12:32)
• attributes in docs (6 messages, latest: Dec 06 2022 at 10:21)
• file not in the list (4 messages, latest: Dec 06 2022 at 10:01)
• typeclass timeout (27 messages, latest: Dec 06 2022 at 07:57)
• symm attribute failure (13 messages, latest: Dec 06 2022 at 04:32)
• status of data.nat.bits (10 messages, latest: Dec 06 2022 at 03:30)
• parsing ⇑ (8 messages, latest: Dec 06 2022 at 01:11)
• symm (7 messages, latest: Dec 05 2022 at 23:33)
• list.traverse (27 messages, latest: Dec 05 2022 at 20:10)
• Porting Algebra.Group.Ext (31 messages, latest: Dec 05 2022 at 13:53)
• Searching a DiscrTree (2 messages, latest: Dec 05 2022 at 11:47)
• mul_equiv.Pi_congr_right_refl (6 messages, latest: Dec 05 2022 at 09:45)
• to_additive and #align (11 messages, latest: Dec 05 2022 at 00:04)
• to_additive and coe (20 messages, latest: Dec 04 2022 at 22:25)
• data.real.basic (12 messages, latest: Dec 04 2022 at 17:51)
• plan for data.json? (8 messages, latest: Dec 04 2022 at 16:05)
• data.list.defs mathlib4#803 (3 messages, latest: Dec 04 2022 at 16:02)
• Pretty-printing binary operations (19 messages, latest: Dec 04 2022 at 15:59)
• mapM' (12 messages, latest: Dec 04 2022 at 11:02)
• by { } (30 messages, latest: Dec 04 2022 at 10:37)
• Functor.map name collision (16 messages, latest: Dec 04 2022 at 01:56)
• (Has)InvolutiveInv (9 messages, latest: Dec 04 2022 at 01:35)
• _proof_1 (2 messages, latest: Dec 04 2022 at 01:29)
• mathlib4#838 (3 messages, latest: Dec 03 2022 at 20:26)
• monotoneOn_univ (4 messages, latest: Dec 03 2022 at 17:15)
• message in mathlib3port file (23 messages, latest: Dec 03 2022 at 17:04)
• porting instructions: runLinter? (1 message, latest: Dec 03 2022 at 14:40)
• lean3port (17 messages, latest: Dec 03 2022 at 14:36)
• Algebra.Ring.Basic (25 messages, latest: Dec 03 2022 at 13:59)
• intermediate versions (11 messages, latest: Dec 03 2022 at 00:22)
• algebra.group.with_one (11 messages, latest: Dec 02 2022 at 23:46)
• instance loop? (39 messages, latest: Dec 02 2022 at 23:21)
• Status of data.list.defs? (48 messages, latest: Dec 02 2022 at 22:19)
• Semigroup.to_isAssociative (9 messages, latest: Dec 02 2022 at 20:51)
• Field notation and CoeFun (28 messages, latest: Dec 02 2022 at 20:28)
• lean_core.data.vector (4 messages, latest: Dec 02 2022 at 19:28)
• Porting CategoryTheory.NaturalIso (11 messages, latest: Dec 02 2022 at 17:45)
• modified since verified (46 messages, latest: Dec 02 2022 at 11:34)
• mathlib4#665 - Data.Stream.Defs (11 messages, latest: Dec 02 2022 at 10:07)
• Path Sequences (18 messages, latest: Dec 02 2022 at 07:56)
• Missing Lean 4 defs (12 messages, latest: Dec 01 2022 at 21:09)
• how to configure jump to definition (11 messages, latest: Dec 01 2022 at 20:52)
• Failure to synthesize instance (11 messages, latest: Dec 01 2022 at 17:54)
• how does one get a higher_order annotation in Lean 4? (4 messages, latest: Dec 01 2022 at 16:12)
• Applicative variants of Monadic functions (4 messages, latest: Dec 01 2022 at 15:58)
• why dubious? (8 messages, latest: Dec 01 2022 at 07:52)
• List.head (14 messages, latest: Dec 01 2022 at 05:08)
• Algebra.Field.Defs mathlib4#668 (12 messages, latest: Nov 30 2022 at 23:55)
• commit convention (13 messages, latest: Nov 30 2022 at 18:11)
• mathport/align questions (5 messages, latest: Nov 30 2022 at 17:51)
• Sigma types or Parameters? (7 messages, latest: Nov 30 2022 at 16:05)
• control_laws_tac (3 messages, latest: Nov 30 2022 at 13:17)
• computability (3 messages, latest: Nov 30 2022 at 09:39)
• data.nat.basic mathlib4#729 (1 message, latest: Nov 30 2022 at 08:11)
• mathlib4#793 (3 messages, latest: Nov 30 2022 at 02:40)
• ext.1 (5 messages, latest: Nov 30 2022 at 00:15)
• data.nat.basic mathlib3#729 (3 messages, latest: Nov 30 2022 at 00:05)
• multiple environment changing attributes (8 messages, latest: Nov 30 2022 at 00:00)
• MonadRun (5 messages, latest: Nov 29 2022 at 23:47)
• congrArg or congr_arg (5 messages, latest: Nov 29 2022 at 22:45)
• min and max in LinearOrder (2 messages, latest: Nov 29 2022 at 21:25)
• submodules (59 messages, latest: Nov 29 2022 at 20:55)
• Pretty printing of existential quantifier broken (11 messages, latest: Nov 29 2022 at 20:51)
• What to port? (15 messages, latest: Nov 29 2022 at 20:35)
• simp (17 messages, latest: Nov 29 2022 at 19:48)
• category theory (1 message, latest: Nov 29 2022 at 19:27)
• mathlib4#659 Algebra.Hom.Group (12 messages, latest: Nov 29 2022 at 19:18)
• Prod.Lex vs Lex (6 messages, latest: Nov 29 2022 at 18:05)
• instance search sees through type synonyms (4 messages, latest: Nov 29 2022 at 17:53)
• Std4 vs Mathlib4 (5 messages, latest: Nov 29 2022 at 16:56)
• xor for Bool (9 messages, latest: Nov 29 2022 at 16:49)
• style of multiple if let expressions (12 messages, latest: Nov 29 2022 at 15:54)
• fatal: ambiguous argument 'mathlib4#771..HEAD' (5 messages, latest: Nov 29 2022 at 07:58)
• porting has_reflected and friends (15 messages, latest: Nov 28 2022 at 22:36)
• ✔ OrderTop.ext_top (7 messages, latest: Nov 28 2022 at 22:30)
• type synonym trickery not working (20 messages, latest: Nov 28 2022 at 21:00)
• requesting help on mathlib4#674 (24 messages, latest: Nov 28 2022 at 17:00)
• leanproject errors with import-graph, etc (5 messages, latest: Nov 28 2022 at 16:38)
• OrderTop.ext_top (5 messages, latest: Nov 28 2022 at 13:51)
• to_additive instance priority (11 messages, latest: Nov 28 2022 at 13:19)
• ✔ More to_additive issues (10 messages, latest: Nov 28 2022 at 11:09)
• ENnReal (61 messages, latest: Nov 28 2022 at 09:07)
• mathlib#17733 (8 messages, latest: Nov 28 2022 at 09:05)
• Subtype.val not a coe (54 messages, latest: Nov 28 2022 at 03:24)
• More to_additive issues (4 messages, latest: Nov 28 2022 at 01:37)
• Implicit arguments in definition of subset (8 messages, latest: Nov 27 2022 at 22:08)
• splitting order.bounded_order (8 messages, latest: Nov 27 2022 at 19:58)
• withMainContext (7 messages, latest: Nov 27 2022 at 07:34)
• Coe, CoeHead, CoeTail (18 messages, latest: Nov 27 2022 at 04:54)
• FAQ on porting (22 messages, latest: Nov 27 2022 at 03:33)
• non defeq in mathlib4#735 (6 messages, latest: Nov 26 2022 at 22:23)
• naming ext lemmas (2 messages, latest: Nov 26 2022 at 20:10)
• Naming for forall/exists as theorem names (9 messages, latest: Nov 26 2022 at 18:33)
• proof review in mathlib4#728 (14 messages, latest: Nov 26 2022 at 18:26)
• default files (33 messages, latest: Nov 26 2022 at 16:44)
• ✔ github access (2 messages, latest: Nov 25 2022 at 22:09)
• github access (4 messages, latest: Nov 25 2022 at 21:55)
• Nat.find (1 message, latest: Nov 25 2022 at 19:55)
• mysterious error related to outParam (1 message, latest: Nov 25 2022 at 19:51)
• list.nth_le (7 messages, latest: Nov 25 2022 at 08:21)
• Defanging the unnecessary seqFocus linter (4 messages, latest: Nov 24 2022 at 23:23)
• List-like interface for String? (7 messages, latest: Nov 24 2022 at 22:21)
• GroupWithZero extends (2 messages, latest: Nov 24 2022 at 20:07)
• Nudge porting move_add (1 message, latest: Nov 24 2022 at 18:27)
• Can someone explain what's going on here? (15 messages, latest: Nov 24 2022 at 17:58)
• instances are no longer protected (9 messages, latest: Nov 24 2022 at 17:55)
• Logic for ULift lemmas (2 messages, latest: Nov 24 2022 at 15:08)
• to_additive issues (56 messages, latest: Nov 24 2022 at 08:06)
• Prop-valued field names (33 messages, latest: Nov 24 2022 at 06:59)
• Naming for prop valued structure fields (2 messages, latest: Nov 24 2022 at 03:52)
• to_additive and iffs with Exists (21 messages, latest: Nov 24 2022 at 01:53)
• data.set.finite (40 messages, latest: Nov 24 2022 at 00:13)
• Naming & notation: Algebra.Order.AbsoluteValue (4 messages, latest: Nov 23 2022 at 22:18)
• editing PRs (1 message, latest: Nov 23 2022 at 20:33)
• logic.equiv.basic mathlib4#631 (53 messages, latest: Nov 23 2022 at 19:09)
• Procedure for using add_port_comments.py (4 messages, latest: Nov 23 2022 at 19:00)
• Set notation (6 messages, latest: Nov 23 2022 at 17:55)
• algebra.order.field.power missing (21 messages, latest: Nov 23 2022 at 17:48)
• merge powers (1 message, latest: Nov 23 2022 at 13:35)
• PR #15691 (1 message, latest: Nov 23 2022 at 10:55)
• ↑1 = 1? (10 messages, latest: Nov 23 2022 at 10:54)
• ✔ Dependency between branches on mathlib4 (4 messages, latest: Nov 22 2022 at 21:39)
• 11-20 nightly mathlib3port (15 messages, latest: Nov 22 2022 at 20:05)
• to_additive and instances (11 messages, latest: Nov 22 2022 at 14:06)
• LibrarySearch application type mismatch (Nat + Subsingleton) (16 messages, latest: Nov 22 2022 at 04:36)
• mathlib4#588 (10 messages, latest: Nov 22 2022 at 00:02)
• mathlib4#549 (3 messages, latest: Nov 21 2022 at 23:47)
• What does simpa using foo do? (34 messages, latest: Nov 21 2022 at 21:14)
• recursive definitions in instance fields (22 messages, latest: Nov 21 2022 at 19:44)
• to_additive thinks it's in a namespace (3 messages, latest: Nov 21 2022 at 09:42)
• import-graph lookahead (9 messages, latest: Nov 21 2022 at 08:50)
• debug simp max recursion depth reached (3 messages, latest: Nov 21 2022 at 03:44)
• What files were ported in #641? (22 messages, latest: Nov 21 2022 at 02:54)
• old_structure_cmd (13 messages, latest: Nov 21 2022 at 00:33)
• Instance search for nat pow times out (4 messages, latest: Nov 20 2022 at 23:20)
• Status of Algebra.Group.Commute? (2 messages, latest: Nov 20 2022 at 21:30)
• checking that mathbin and mathlib port capture decls (6 messages, latest: Nov 20 2022 at 21:09)
• porting tool assistance (7 messages, latest: Nov 20 2022 at 19:22)
• 1+1 = 2 (10 messages, latest: Nov 20 2022 at 14:03)
• data.stream.defs (6 messages, latest: Nov 20 2022 at 12:14)
• add_port_comments.py (11 messages, latest: Nov 20 2022 at 12:06)
• mathlib4#655 (10 messages, latest: Nov 20 2022 at 09:38)
• help with a failing to_additive (26 messages, latest: Nov 20 2022 at 09:23)
• Linting standards for mathlib (23 messages, latest: Nov 20 2022 at 08:28)
• Universe lint & Ulift (21 messages, latest: Nov 20 2022 at 07:11)
• pi_instance(_derive_field): possible changes? (9 messages, latest: Nov 20 2022 at 02:13)
• EmbeddingLike (10 messages, latest: Nov 20 2022 at 01:18)
• Do port status scripts belong in mathlibtools or mathlib? (9 messages, latest: Nov 20 2022 at 00:33)
• algebra.hierarchy_design (7 messages, latest: Nov 19 2022 at 23:13)
• ✔ "Theory development" VS "tactic porting" (3 messages, latest: Nov 19 2022 at 19:12)
• max_default/min_default (8 messages, latest: Nov 19 2022 at 10:07)
• porting lazylist (7 messages, latest: Nov 19 2022 at 07:35)
• Should we mark Mathlib.Data.RBTree.* as ported? (7 messages, latest: Nov 19 2022 at 01:33)
• multifile PRs (3 messages, latest: Nov 19 2022 at 00:37)
• How to clone mathlib4 (17 messages, latest: Nov 18 2022 at 22:20)
• Option.get (5 messages, latest: Nov 18 2022 at 22:04)
• solve two goals with [tac1,tac2] (2 messages, latest: Nov 18 2022 at 22:04)
• Documentation on lint overrides? (5 messages, latest: Nov 18 2022 at 21:56)
• default proofs (17 messages, latest: Nov 18 2022 at 21:54)
• align tag (4 messages, latest: Nov 18 2022 at 21:26)
• capitals in Logic.Equiv.Defs file (13 messages, latest: Nov 18 2022 at 21:15)
• double-capital identifiers (9 messages, latest: Nov 18 2022 at 20:57)
• congr attribute (7 messages, latest: Nov 18 2022 at 20:10)
• porting Algebra/Quotient (9 messages, latest: Nov 18 2022 at 12:39)
• Porting monads (23 messages, latest: Nov 18 2022 at 10:59)
• simp on Compares downstream effects (5 messages, latest: Nov 18 2022 at 03:12)
• Docstring style? (4 messages, latest: Nov 18 2022 at 00:52)
• mathlib4#560 (14 messages, latest: Nov 18 2022 at 00:36)
• logic.equiv.defs mathlib4#550 (3 messages, latest: Nov 18 2022 at 00:22)
• good first port – good beginner files (11 messages, latest: Nov 17 2022 at 23:57)
• CI for checking files are imported (5 messages, latest: Nov 17 2022 at 23:01)
• printing inferInstance (4 messages, latest: Nov 17 2022 at 22:45)
• Linting in VS code (14 messages, latest: Nov 17 2022 at 22:41)
• data.nat.cast.defs (17 messages, latest: Nov 17 2022 at 20:34)
• protecting structure projections (3 messages, latest: Nov 17 2022 at 19:41)
• dsimp and simp (5 messages, latest: Nov 17 2022 at 19:39)
• porting localized (42 messages, latest: Nov 17 2022 at 19:37)
• data.sigma.default (20 messages, latest: Nov 17 2022 at 19:01)
• vscode with remote repositories failing to find toolchain (5 messages, latest: Nov 17 2022 at 13:53)
• to_additive and noncomputable (2 messages, latest: Nov 17 2022 at 13:42)
• Local notation (8 messages, latest: Nov 17 2022 at 13:37)
• mathlib4#604 (3 messages, latest: Nov 17 2022 at 11:33)
• Zulip shortcuts (9 messages, latest: Nov 17 2022 at 07:03)
• How to help (9 messages, latest: Nov 17 2022 at 05:43)
• zify (34 messages, latest: Nov 17 2022 at 05:08)
• missing tactic port (37 messages, latest: Nov 17 2022 at 03:57)
• auto_param.check_exists in ported file (4 messages, latest: Nov 17 2022 at 00:44)
• Catalog of porting patterns? (4 messages, latest: Nov 16 2022 at 17:03)
• Check that all files are imported (8 messages, latest: Nov 16 2022 at 15:18)
• #align in namespaces (4 messages, latest: Nov 16 2022 at 11:57)
• capitalisation and dot notation (5 messages, latest: Nov 16 2022 at 11:23)
• Linting (15 messages, latest: Nov 16 2022 at 10:40)
• fixing easy error in Mathbin (4 messages, latest: Nov 16 2022 at 10:35)
• by_cases spacing (2 messages, latest: Nov 16 2022 at 10:14)
• has_seq vs Seq (2 messages, latest: Nov 16 2022 at 07:57)
• Should mllist be MLList (6 messages, latest: Nov 16 2022 at 05:07)
• verifying ported files against mathlib (25 messages, latest: Nov 16 2022 at 04:45)
• How to find instances (11 messages, latest: Nov 15 2022 at 20:43)
• has_reflect (14 messages, latest: Nov 15 2022 at 20:28)
• aligns without content? (4 messages, latest: Nov 15 2022 at 20:17)
• style guide (2 messages, latest: Nov 15 2022 at 19:39)
• simp timeing out (15 messages, latest: Nov 15 2022 at 05:56)
• some useful automation (73 messages, latest: Nov 15 2022 at 04:01)
• Basic porting questions (6 messages, latest: Nov 14 2022 at 20:53)
• using eta-rfl for Equiv (16 messages, latest: Nov 14 2022 at 15:01)
• logic.equiv.defs causing elaboration issues in Simps tests (4 messages, latest: Nov 14 2022 at 08:08)
• "Ported by:" docstring (5 messages, latest: Nov 13 2022 at 16:26)
• protecting master (1 message, latest: Nov 13 2022 at 06:36)
• best way to help? (27 messages, latest: Nov 13 2022 at 05:43)
• linear order on Int (3 messages, latest: Nov 11 2022 at 12:55)
• simp! does not unfold abbrevs (2 messages, latest: Nov 11 2022 at 04:17)
• congr_arg not unifying HMul (3 messages, latest: Nov 11 2022 at 04:07)
• rw side goal proofs (7 messages, latest: Nov 11 2022 at 04:04)
• simpNF error "unknown metavariable" (10 messages, latest: Nov 11 2022 at 03:57)
• Omitting indexing type in a pi type (6 messages, latest: Nov 11 2022 at 00:45)
• to_additive (2 messages, latest: Nov 10 2022 at 13:32)
• Updating mathlib3port (22 messages, latest: Nov 09 2022 at 17:39)
• ∃ {n : ℕ} (14 messages, latest: Nov 09 2022 at 15:59)
• eqv_gen (6 messages, latest: Nov 09 2022 at 15:20)
• indentation (6 messages, latest: Nov 09 2022 at 13:49)
• mathlib4#557 (15 messages, latest: Nov 09 2022 at 07:02)
• root (5 messages, latest: Nov 08 2022 at 23:04)
• Using inferInstance as partial fills in instance defs (18 messages, latest: Nov 08 2022 at 04:36)
• Equality of structures with autoparams (15 messages, latest: Nov 07 2022 at 19:12)
• to_additive on structures (4 messages, latest: Nov 07 2022 at 04:34)
• align for Repr.reprPrec (3 messages, latest: Nov 07 2022 at 04:15)
• LinearOrder in mathlib3/4 (14 messages, latest: Nov 07 2022 at 03:42)
• mathlib4#537 (2 messages, latest: Nov 06 2022 at 08:42)
• norm_num for non-semirings (9 messages, latest: Nov 05 2022 at 20:27)
• equivalence relations are symmetric (7 messages, latest: Nov 05 2022 at 12:25)
• attribute [instance, priority 10] coe_fn_trans (4 messages, latest: Nov 05 2022 at 04:54)
• include/omit (3 messages, latest: Nov 05 2022 at 03:39)
• mathlib 3 ready to merge PR (3 messages, latest: Nov 05 2022 at 02:59)
• [RFC] refine_struct functionality via new ?.. syntax (1 message, latest: Nov 04 2022 at 02:08)
• refine_struct (4 messages, latest: Nov 03 2022 at 22:23)
• convert_to (20 messages, latest: Nov 01 2022 at 23:39)
• zify mathlib4#517 (3 messages, latest: Oct 31 2022 at 05:22)
• need help placating simpNF linter (45 messages, latest: Oct 30 2022 at 15:08)
• #align bug when already aligned (2 messages, latest: Oct 30 2022 at 14:28)
• Porting status for lean3 core (12 messages, latest: Oct 30 2022 at 07:05)
• Importing a file changed dite if macro semantics (7 messages, latest: Oct 30 2022 at 04:45)
• how to include mathlib4 in the lakefile? (6 messages, latest: Oct 28 2022 at 22:58)
• mathlib4#511 (4 messages, latest: Oct 28 2022 at 22:29)
• ✔ invalid simp theorem (2 messages, latest: Oct 28 2022 at 18:20)
• invalid simp theorem (3 messages, latest: Oct 28 2022 at 18:18)
• List and monads (4 messages, latest: Oct 27 2022 at 09:16)
• Move some tactics to separate package? (8 messages, latest: Oct 27 2022 at 01:08)
• Injective (15 messages, latest: Oct 25 2022 at 00:46)
• xor (2 messages, latest: Oct 24 2022 at 21:19)
• and_self (5 messages, latest: Oct 24 2022 at 21:09)
• error while loading shared libraries (2 messages, latest: Oct 24 2022 at 20:35)
• to_additive and smul (4 messages, latest: Oct 24 2022 at 11:15)
• tooling (1 message, latest: Oct 24 2022 at 10:30)
• unusedArguments linter not referencing nolints (6 messages, latest: Oct 24 2022 at 05:42)
• Should boolean or_assoc be a simp lemma? (10 messages, latest: Oct 24 2022 at 03:26)
• local notation for subtypes (4 messages, latest: Oct 23 2022 at 23:37)
• porting core Lean 3 stuff? (9 messages, latest: Oct 23 2022 at 22:12)
• lean 3/4 bool ! precedence (3 messages, latest: Oct 21 2022 at 20:53)
• porting logic.basic (54 messages, latest: Oct 21 2022 at 10:42)
• toBool (23 messages, latest: Oct 21 2022 at 08:25)
• data.option.defs (6 messages, latest: Oct 21 2022 at 07:35)
• porting algebra.order.ring_lemmas (5 messages, latest: Oct 20 2022 at 18:32)
• [t1, …, tn] combinator (5 messages, latest: Oct 20 2022 at 10:26)
• dropping import Mathbin support (1 message, latest: Oct 20 2022 at 04:45)
• Exists.some_spec alignment seems to not be working (6 messages, latest: Oct 20 2022 at 04:08)
• proposal for marking files as frozen (115 messages, latest: Oct 20 2022 at 01:14)
• to_additive and multiple parents (3 messages, latest: Oct 20 2022 at 00:34)
• error when executing port status script (6 messages, latest: Oct 19 2022 at 22:43)
• porting data.bool.basic (3 messages, latest: Oct 19 2022 at 19:47)
• importing binported oleans (1 message, latest: Oct 19 2022 at 18:33)
• porting data.sigma.basic (29 messages, latest: Oct 19 2022 at 12:05)
• linting (2 messages, latest: Oct 18 2022 at 20:42)
• empty type (8 messages, latest: Oct 18 2022 at 18:21)
• porting questions (9 messages, latest: Oct 18 2022 at 17:11)
• ring failure (2 messages, latest: Oct 18 2022 at 16:31)
• is_refl (25 messages, latest: Oct 18 2022 at 00:06)
• Understanding tauto.lean (mathlib3) (60 messages, latest: Oct 17 2022 at 23:33)
• problem with change (18 messages, latest: Oct 17 2022 at 18:31)
• missing attributes (6 messages, latest: Oct 17 2022 at 07:23)
• Using QQ when you only have an Expr (6 messages, latest: Oct 17 2022 at 03:11)
• Some naming questions (15 messages, latest: Oct 16 2022 at 22:00)
• data.prod (3 messages, latest: Oct 16 2022 at 20:24)
• status of ring (9 messages, latest: Oct 14 2022 at 10:32)
• elaborate context in attributes (15 messages, latest: Oct 13 2022 at 21:02)
• porting names (7 messages, latest: Oct 11 2022 at 14:22)
• A QQ about Nat (4 messages, latest: Oct 11 2022 at 04:37)
• weirdness with ofNat (3 messages, latest: Oct 11 2022 at 04:15)
• Changed API for SatisfiesM_mapIdxM.go (2 messages, latest: Oct 10 2022 at 21:00)
• by_contra when goal is an implication (6 messages, latest: Oct 10 2022 at 20:41)
• #457 (40 messages, latest: Oct 10 2022 at 03:31)
• Which files to port? (203 messages, latest: Oct 08 2022 at 04:52)
• solve_aux (9 messages, latest: Oct 06 2022 at 04:32)
• DecidableEq vs BEq and LawfulHashable (5 messages, latest: Oct 04 2022 at 17:20)
• rfl tactic (42 messages, latest: Sep 29 2022 at 18:29)
• using binport only (136 messages, latest: Sep 28 2022 at 20:17)
• using mathlib3port (7 messages, latest: Sep 24 2022 at 02:52)
• mathlib4 vs std4 (3 messages, latest: Sep 22 2022 at 18:00)
• difficulty porting List.perm_inv_core (10 messages, latest: Sep 19 2022 at 04:57)
• rfl tactic (1 message, latest: Sep 18 2022 at 21:22)
• guardHyp (14 messages, latest: Sep 18 2022 at 20:48)
• choose (48 messages, latest: Sep 17 2022 at 14:47)
• dsimp conv (16 messages, latest: Sep 16 2022 at 18:17)
• Deprecated defs (5 messages, latest: Sep 16 2022 at 03:39)
• Exists Unique (2 messages, latest: Sep 13 2022 at 10:20)
• wlog (10 messages, latest: Sep 13 2022 at 08:47)
• ✔ existsi (3 messages, latest: Sep 09 2022 at 17:07)
• trying to run mathport (30 messages, latest: Sep 09 2022 at 13:29)
• cc (6 messages, latest: Sep 08 2022 at 15:47)
• mapply (2 messages, latest: Sep 06 2022 at 05:43)
• Building mathlib 4 (1 message, latest: Sep 02 2022 at 05:07)
• status of binport syntax (5 messages, latest: Aug 31 2022 at 13:49)
• Changing instance priority (14 messages, latest: Aug 07 2022 at 02:28)
• Do we still have plenty of time before the port? (4 messages, latest: Aug 03 2022 at 16:36)
• Mathlib/Lean/ vs Mathlib/Util/ (5 messages, latest: Jul 27 2022 at 01:33)
• mathlib4#342 (1 message, latest: Jul 23 2022 at 22:03)
• Tensor product of bounded operators (3 messages, latest: Jul 22 2022 at 18:46)
• mathport: cases_on => casesOn (30 messages, latest: Jun 30 2022 at 19:38)
• porting progress (23 messages, latest: Jun 28 2022 at 12:37)
• mathlib4 priorities (22 messages, latest: Jun 27 2022 at 17:58)
• mathport improvements for data.num.add (14 messages, latest: Jun 27 2022 at 16:25)
• ✔ can't import tactic (1 message, latest: May 23 2022 at 13:39)
• can't import tactic (5 messages, latest: May 23 2022 at 13:03)
• Porting streams (Nat → α) (10 messages, latest: May 20 2022 at 13:12)
• ✔ left and right tactics (1 message, latest: May 03 2022 at 15:54)
• left and right tactics (2 messages, latest: May 03 2022 at 12:46)
• ✔ autoImplicit confusion? (1 message, latest: Apr 29 2022 at 09:26)
• autoImplicit confusion? (3 messages, latest: Apr 29 2022 at 02:13)
• (interactive) conv mode (25 messages, latest: Apr 28 2022 at 11:44)
• mathlib newbie issue: exists tactic (10 messages, latest: Apr 25 2022 at 23:55)
• Fixing rcases for nightly (8 messages, latest: Apr 20 2022 at 08:24)
• Symm and Trans tactics implementation (2 messages, latest: Apr 06 2022 at 05:26)
• lean core nightly bump (6 messages, latest: Apr 05 2022 at 16:37)
• Symm tactic implementation (13 messages, latest: Apr 05 2022 at 11:14)
• Propagate Tags (10 messages, latest: Apr 05 2022 at 00:48)
• Syntax triage (13 messages, latest: Apr 04 2022 at 14:11)
• Proof of false using library_search (12 messages, latest: Apr 03 2022 at 02:35)
• set tactic and elab benefits? (25 messages, latest: Mar 23 2022 at 18:43)
• ✔ congr tactic: first steps (8 messages, latest: Mar 23 2022 at 07:41)
• congr tactic: first steps (76 messages, latest: Mar 23 2022 at 06:52)
• Push_neg port (4 messages, latest: Mar 21 2022 at 07:55)
• expand have capabilities (162 messages, latest: Mar 18 2022 at 23:56)
• replace tactic (23 messages, latest: Mar 17 2022 at 18:18)
• Installation demo (8 messages, latest: Mar 17 2022 at 13:39)
• port unfold_wf (1 message, latest: Mar 16 2022 at 20:06)
• prioritizing porting efforts (18 messages, latest: Mar 16 2022 at 09:15)
• ✔ simpa tactic (1 message, latest: Mar 15 2022 at 20:40)
• is restate_axiom needed? (8 messages, latest: Mar 15 2022 at 19:23)
• squeeze_simp and simp? (38 messages, latest: Mar 15 2022 at 18:30)
• simpa tactic (32 messages, latest: Mar 14 2022 at 19:16)
• getting started with joining the porting effort (9 messages, latest: Mar 14 2022 at 10:11)
• State of mathlib4? (4 messages, latest: Mar 12 2022 at 18:49)
• work_on_goal vs swap (68 messages, latest: Mar 04 2022 at 12:12)
• Tactic status? (169 messages, latest: Mar 01 2022 at 13:30)
• independent and auxiliary (10 messages, latest: Feb 21 2022 at 21:41)
• adding to std (20 messages, latest: Feb 20 2022 at 13:50)
• mathlib4 as a dependency? (11 messages, latest: Feb 19 2022 at 20:27)
• Q. about ByteSlice.getOp (29 messages, latest: Feb 11 2022 at 05:33)
• tests that expect failure (3 messages, latest: Feb 06 2022 at 19:25)
• swap semantics tactics names (44 messages, latest: Feb 05 2022 at 01:23)
• swap semantics (32 messages, latest: Feb 04 2022 at 19:06)
• Tatic equivalent (4 messages, latest: Feb 03 2022 at 17:28)
• mathlib3port as a dependency (8 messages, latest: Jan 28 2022 at 16:19)
• Ring tactic bug? (8 messages, latest: Jan 25 2022 at 23:10)
• ✔ When mathlib4 (5 messages, latest: Jan 23 2022 at 20:47)
• When mathlib4 (5 messages, latest: Jan 22 2022 at 23:06)
• import data.nat (4 messages, latest: Jan 11 2022 at 16:19)
• Aggressiveness of nat literal conversion (6 messages, latest: Jan 11 2022 at 07:50)
• Explicit/implicit argument of Inhabited.default (12 messages, latest: Jan 07 2022 at 14:36)
• is mathlib made only by the community? (5 messages, latest: Jan 06 2022 at 02:00)
• Ordered merge slower than append-then-sort (22 messages, latest: Jan 02 2022 at 18:02)
• ✔ New Project that uses MathLib4 (5 messages, latest: Dec 26 2021 at 11:09)
• porting record (1 message, latest: Dec 23 2021 at 07:51)
• Mathport abs syntax clash (21 messages, latest: Dec 14 2021 at 18:07)
• generating Mathlib.lean (6 messages, latest: Dec 14 2021 at 05:24)
• More issues with OfNat (42 messages, latest: Dec 14 2021 at 02:45)
• Signed integers (13 messages, latest: Dec 13 2021 at 21:42)
• Deterministic timeout with Inhabited from Zero (14 messages, latest: Dec 13 2021 at 10:38)
• porting simps and to_additive (99 messages, latest: Dec 09 2021 at 21:48)
• comments (19 messages, latest: Nov 29 2021 at 10:47)
• Renaming split (92 messages, latest: Nov 29 2021 at 04:12)
• Referencing mathlib 4 from module (7 messages, latest: Nov 14 2021 at 00:44)
• mathport re-org (6 messages, latest: Nov 11 2021 at 23:39)
• getting mathlib running (16 messages, latest: Nov 08 2021 at 21:06)
• decide vs Decidable.to_bool (9 messages, latest: Oct 30 2021 at 00:11)
• International docs (10 messages, latest: Oct 27 2021 at 21:27)
• add import Leanbin.Init.Default in synported files (106 messages, latest: Oct 20 2021 at 09:20)
• 0🔶 ("zero diamond") (11 messages, latest: Oct 18 2021 at 17:53)
• ✔ "Use" tactic implementation in lean 4 (12 messages, latest: Oct 18 2021 at 16:42)
• "Use" tactic implementation in lean 4 (7 messages, latest: Oct 18 2021 at 07:45)
• PR to use lake (1 message, latest: Oct 18 2021 at 00:14)
• Update lean? (31 messages, latest: Oct 06 2021 at 02:31)
• Coend calculus in Lean (1 message, latest: Oct 01 2021 at 22:06)
• mathport depending on mathlib (163 messages, latest: Oct 01 2021 at 00:43)
• Porting Nat/Digits (11 messages, latest: Sep 29 2021 at 22:00)
• List.subset weak implicit (4 messages, latest: Sep 27 2021 at 06:13)
• emacs setup (1 message, latest: Sep 22 2021 at 23:12)
• Documentation mistake in algebra.covariant_and_contravariant (6 messages, latest: Sep 12 2021 at 22:21)
• specialize @foo x (4 messages, latest: Sep 08 2021 at 16:06)
• Instance binders in exists (26 messages, latest: Sep 08 2021 at 09:04)
• mathport bump (1 message, latest: Sep 08 2021 at 02:54)
• OfNat/Numeric (15 messages, latest: Sep 03 2021 at 19:46)
• fun with binport (25 messages, latest: Aug 31 2021 at 22:37)
• backport remove cc macros (17 messages, latest: Aug 27 2021 at 14:56)
• purpose of Mathlib.lean file? (24 messages, latest: Aug 25 2021 at 05:37)
• file organization in mathlib4 repo (1 message, latest: Aug 24 2021 at 00:44)
• Alternative MetaM (3 messages, latest: Aug 23 2021 at 05:30)
• Nat.le backport (15 messages, latest: Aug 22 2021 at 15:51)
• mathport clashes (1 message, latest: Aug 21 2021 at 23:42)
• help wanted: strategic binport experimentation (64 messages, latest: Aug 21 2021 at 23:15)
• Building binport (2 messages, latest: Aug 21 2021 at 04:02)
• profiling ring (17 messages, latest: Aug 20 2021 at 02:10)
• bad simp lemmas (30 messages, latest: Aug 18 2021 at 21:50)
• panic while testing ring tactic (12 messages, latest: Aug 18 2021 at 10:29)
• RFC: porting strategies (42 messages, latest: Aug 15 2021 at 23:44)
• structure cmd (7 messages, latest: Aug 11 2021 at 17:25)
• argument order of Or.elim (6 messages, latest: Aug 05 2021 at 19:37)
• Tactic casing convention (67 messages, latest: Jul 30 2021 at 02:10)
• Lean4 math library (3 messages, latest: Jul 23 2021 at 05:45)
• "· tac" block notation (96 messages, latest: Jul 22 2021 at 23:44)
• close branch (5 messages, latest: Jul 12 2021 at 20:25)
• #8190 (4 messages, latest: Jul 04 2021 at 13:42)
• Backporting strict implicits (2 messages, latest: Jul 04 2021 at 07:12)
• Push access to branches? (2 messages, latest: Jul 03 2021 at 21:23)
• Data/Nat/Gcd.lean (2 messages, latest: Jun 21 2021 at 02:27)
• treating mathlib as a stdlib (299 messages, latest: Jun 10 2021 at 21:03)
• Experiments with algebra (5 messages, latest: Jun 04 2021 at 16:21)
• sorry (13 messages, latest: Jun 03 2021 at 16:52)
• github diffs trick (10 messages, latest: May 23 2021 at 13:50)
• Mem notation (1 message, latest: May 23 2021 at 09:42)
• List.mem (9 messages, latest: May 23 2021 at 06:07)
• Schemes (1 message, latest: May 22 2021 at 10:31)
• algebra hierarchy (4 messages, latest: May 18 2021 at 16:43)
• .vscode (2 messages, latest: May 15 2021 at 04:32)

---

Last updated: Dec 20 2023 at 11:08 UTC