Zulip Chat Archive

Stream: maths

---

Topics:

• Moreira-2001 (generalization of Sard's theorem) (36 messages, latest: Dec 20 2025 at 21:18)
• infinite product measure (9 messages, latest: Dec 20 2025 at 19:19)
• mul_pos (42 messages, latest: Dec 19 2025 at 21:25)
• thoughts on elliptic curves (599 messages, latest: Dec 19 2025 at 21:11)
• upper hemicontinuity vs. upper semicontinuity (37 messages, latest: Dec 17 2025 at 17:42)
• Formalizing Jung's theorem and minimal bounding spheres (7 messages, latest: Dec 14 2025 at 14:37)
• Implicit function theorem in familiar form (28 messages, latest: Dec 09 2025 at 20:58)
• Weak-Mixing (Ergodic Theory) (23 messages, latest: Dec 09 2025 at 16:18)
• Ring orderings - structure or predicate? (15 messages, latest: Dec 09 2025 at 03:28)
• measurable space structure on restricted product (11 messages, latest: Dec 08 2025 at 17:17)
• Schwarz-Pick, Grönwall, Bierbach, Koebe (1 message, latest: Dec 07 2025 at 22:02)
• IsCancelMulZero and NoZeroDivisors for semirings (7 messages, latest: Dec 07 2025 at 20:31)
• Looking for feedback: Coloured operads formalization (24 messages, latest: Dec 06 2025 at 10:19)
• Categorical logic in Lean? (algebraic theories, etc.) (94 messages, latest: Dec 05 2025 at 14:00)
• Ring of integers in quadratic fields (11 messages, latest: Dec 02 2025 at 09:17)
• Euler-Maclaurin formula (11 messages, latest: Nov 30 2025 at 19:16)
• Isoperimetric Inequality (29 messages, latest: Nov 27 2025 at 20:10)
• Formalizing Perron-Frobenius (21 messages, latest: Nov 27 2025 at 13:27)
• classification of finite subgroups of SL(2,F) (147 messages, latest: Nov 26 2025 at 16:47)
• Linear independence over semirings (47 messages, latest: Nov 26 2025 at 09:34)
• Question on gluing schemes (3 messages, latest: Nov 25 2025 at 18:09)
• Affine Combination Space (44 messages, latest: Nov 25 2025 at 00:04)
• Equiv.Perm (Fin (n + 1)) is a Coxeter group (1 message, latest: Nov 24 2025 at 16:33)
• Gelfond-Schneider theorem (3 messages, latest: Nov 24 2025 at 09:35)
• Restricting to a backwards invariant set (31 messages, latest: Nov 21 2025 at 12:34)
• Formalise the proposition P ≠NP (29 messages, latest: Nov 18 2025 at 03:21)
• Refactoring category (3 messages, latest: Nov 16 2025 at 08:47)
• Polyhedra in mathlib (85 messages, latest: Nov 16 2025 at 07:01)
• topological groups and uniformity (27 messages, latest: Nov 14 2025 at 12:54)
• A (very weak!) upper bound on the area of the Mandelbrot set (2 messages, latest: Nov 11 2025 at 21:47)
• On IsModuleTopology (13 messages, latest: Nov 11 2025 at 18:39)
• Polynomials: Irreducible (p.map f) → Irreducible p (34 messages, latest: Nov 11 2025 at 11:40)
• Are Schur number compute NP hard (4 messages, latest: Nov 08 2025 at 13:48)
• Faces of Cones (3 messages, latest: Nov 06 2025 at 16:24)
• Puzzles around Picard group (125 messages, latest: Nov 06 2025 at 10:12)
• Differential geometry problems for undergrad final project? (23 messages, latest: Nov 05 2025 at 11:24)
• Feferman–Vaught (13 messages, latest: Nov 03 2025 at 09:54)
• Continuous Logic (23 messages, latest: Nov 02 2025 at 13:37)
• The product measure is characterized by continuous functions (5 messages, latest: Oct 31 2025 at 20:20)
• Holomorph of a group (10 messages, latest: Oct 30 2025 at 19:21)
• Lattice structure on partitions (54 messages, latest: Oct 29 2025 at 03:33)
• The model category structure on topological spaces (30 messages, latest: Oct 28 2025 at 19:41)
• Union of finsets (6 messages, latest: Oct 26 2025 at 19:57)
• Sequential convergence and countably generated filters (23 messages, latest: Oct 24 2025 at 13:24)
• Serre finiteness theorem formalized in Cubical Agda! (5 messages, latest: Oct 24 2025 at 11:45)
• Showing S : Λ ⟶ ∑₂ is topological conjugacy with μ > 4 (14 messages, latest: Oct 21 2025 at 05:03)
• Consistency strength bounds from Lean proofs (67 messages, latest: Oct 18 2025 at 19:00)
• Difficulty of formalizing a polynomial in Lean4 (22 messages, latest: Oct 18 2025 at 11:51)
• Representation Theory (883 messages, latest: Oct 15 2025 at 00:37)
• Pfaffians? (39 messages, latest: Oct 12 2025 at 14:19)
• Projective Space (215 messages, latest: Oct 10 2025 at 15:46)
• Graph Minors (231 messages, latest: Oct 10 2025 at 13:47)
• locally cartesian closed categories (17 messages, latest: Oct 09 2025 at 21:04)
• How to calculate the number of graphs or trees? (9 messages, latest: Oct 08 2025 at 10:31)
• Lean Formalization of the Riemann Hypothesis – Open for Test (23 messages, latest: Oct 07 2025 at 17:07)
• Normal Closure (4 messages, latest: Oct 07 2025 at 16:38)
• Question about formalization in set theory. (10 messages, latest: Oct 07 2025 at 15:41)
• Local fields in Lean 4 (94 messages, latest: Oct 05 2025 at 10:32)
• Discrete valuation (21 messages, latest: Oct 03 2025 at 15:54)
• combining pullbacks (11 messages, latest: Oct 02 2025 at 16:20)
• Torsors (8 messages, latest: Oct 02 2025 at 03:04)
• Uniqueness of sigma-finite measures on a product space (17 messages, latest: Oct 01 2025 at 09:54)
• How to prove 1/2 is not integral over Z ? (27 messages, latest: Sep 28 2025 at 12:09)
• Dedekind-MacNeille completion (425 messages, latest: Sep 26 2025 at 14:38)
• Reverse mathematics and Dirichlet's theorem(Arithmetic prog) (11 messages, latest: Sep 25 2025 at 11:13)
• Leading term of valuation (134 messages, latest: Sep 25 2025 at 02:03)
• How to formalize (3x - 2y)¹⁸ Expansion Coefficient? (8 messages, latest: Sep 24 2025 at 10:41)
• Is there a Float.pi (15 messages, latest: Sep 24 2025 at 10:08)
• Collinearity in an isosceles triangle (29 messages, latest: Sep 21 2025 at 23:39)
• [Non-matrix example of f-d simple central -ordered algebra?](topic/Non-matrix.20example.20of.20f-d.20simple.20central.20-ordered.20algebra.3F.html) (13 messages, latest: Sep 19 2025 at 18:33)
• Eigenvectors for semirings (10 messages, latest: Sep 17 2025 at 10:47)
• Modular curves (21 messages, latest: Sep 16 2025 at 16:32)
• p-norms on Matrices (13 messages, latest: Sep 13 2025 at 08:10)
• (Z/6Z)[X] (14 messages, latest: Sep 13 2025 at 00:55)
• Schemes over fields and base change (9 messages, latest: Sep 12 2025 at 16:44)
• When the fraction ring is a field (4 messages, latest: Sep 10 2025 at 23:33)
• A theorem about 2-Norm on Matrices (6 messages, latest: Sep 10 2025 at 16:59)
• Problems of Linear Algebra (9 messages, latest: Sep 10 2025 at 15:13)
• Group with zeros (DivisionMonoid thoughts) (2 messages, latest: Sep 05 2025 at 05:44)
• Getting the manifold from a Lie group (6 messages, latest: Sep 05 2025 at 05:38)
• Is this formula a thing? (14 messages, latest: Sep 04 2025 at 22:01)
• Project: Brunerie infinity-groupoids (4 messages, latest: Sep 02 2025 at 05:44)
• Two-open one-closed topology as a limit (7 messages, latest: Sep 01 2025 at 21:14)
• Invertible and data (160 messages, latest: Sep 01 2025 at 06:53)
• "Uniformity within" filter (119 messages, latest: Aug 30 2025 at 02:14)
• Weil Positivity Criterion (7 messages, latest: Aug 29 2025 at 10:00)
• Ext and Tor (120 messages, latest: Aug 28 2025 at 10:36)
• Condition for sheaf equivalence (5 messages, latest: Aug 26 2025 at 22:11)
• General statement of Ax-Grothendieck (43 messages, latest: Aug 23 2025 at 17:26)
• (Relative) CW complex is T2 (3 messages, latest: Aug 22 2025 at 15:36)
• Gaussian Integration by Parts (Stein's Lemma) - 1D + Hilbert (1 message, latest: Aug 21 2025 at 18:06)
• Complex dynamics and potential theory (20 messages, latest: Aug 21 2025 at 09:21)
• Grothendieck topologies from morphism properties (12 messages, latest: Aug 20 2025 at 08:52)
• "Database of Ring Theory" (10 messages, latest: Aug 20 2025 at 06:31)
• Nimbers (173 messages, latest: Aug 17 2025 at 19:36)
• C1 fields? (26 messages, latest: Aug 13 2025 at 21:50)
• Learning category theory, how do define a certain poset cat? (14 messages, latest: Aug 11 2025 at 05:48)
• "Commensurate" elements in fields (137 messages, latest: Aug 10 2025 at 20:14)
• Proof of Linear Regression Minimizing the Minimum Squar… (5 messages, latest: Aug 06 2025 at 22:32)
• Order-reversing maps (15 messages, latest: Jul 30 2025 at 17:48)
• Birational Geometry (2 messages, latest: Jul 29 2025 at 16:08)
• How to formalize the Odd/Distinct Partition Bijection? (7 messages, latest: Jul 29 2025 at 00:13)
• Refactoring AttachCells (18 messages, latest: Jul 27 2025 at 09:55)
• Riddle about SeminormedAddGroup (10 messages, latest: Jul 24 2025 at 12:26)
• Eigenvalues of Cartan matrices (28 messages, latest: Jul 23 2025 at 09:50)
• Learning Lean through developing ZFC set theory (11 messages, latest: Jul 22 2025 at 23:26)
• Dimensional Analysis Revisited (27 messages, latest: Jul 22 2025 at 23:17)
• A thought on Langlands etc. (2 messages, latest: Jul 21 2025 at 17:08)
• Class Field Theory in Oxford (8 messages, latest: Jul 20 2025 at 21:02)
• Feasibility of formalizing Grid Homology for summer pro… (14 messages, latest: Jul 20 2025 at 21:01)
• "Canonicalize" an algebra (9 messages, latest: Jul 20 2025 at 09:49)
• Proof in Lean 4 formalization of circuits (8 messages, latest: Jul 18 2025 at 06:20)
• Pi.Lex complete linear order (61 messages, latest: Jul 17 2025 at 23:15)
• Refactor AlgebraicGeometry.Scheme.Cover (10 messages, latest: Jul 16 2025 at 23:44)
• Question about Valued.is_topological_valuation (67 messages, latest: Jul 11 2025 at 07:04)
• Partial homeomorphism of open cells in a CW complex (23 messages, latest: Jul 09 2025 at 22:06)
• disjoint union (5 messages, latest: Jul 09 2025 at 20:45)
• ✔ Algebraic Closure (12 messages, latest: Jul 08 2025 at 16:39)
• Roadmap to high school geometry (42 messages, latest: Jul 08 2025 at 10:17)
• what's the status of random matrix theory? (21 messages, latest: Jul 07 2025 at 23:52)
• Type 0 contains a universe (60 messages, latest: Jul 06 2025 at 17:02)
• Completed proof of the Brouwer Fixed Point Theorem (28 messages, latest: Jul 05 2025 at 05:20)
• Unable to prove Matrix lemma (2 messages, latest: Jul 04 2025 at 08:36)
• ✔ cont inj hom between profinite groups induces homeomorp… (5 messages, latest: Jul 02 2025 at 19:27)
• The consistency of NF (145 messages, latest: Jul 01 2025 at 15:50)
• Cardinality of ZFSet (86 messages, latest: Jun 30 2025 at 23:17)
• Computable algebraic integers (13 messages, latest: Jun 30 2025 at 15:47)
• Trouble with tensor product and submatrix proof (14 messages, latest: Jun 27 2025 at 13:19)
• tarski axiom geometry (116 messages, latest: Jun 26 2025 at 09:44)
• Grassmannians (80 messages, latest: Jun 25 2025 at 22:39)
• ✔ Sylow p-subgroup is normal, then it is unique. (19 messages, latest: Jun 25 2025 at 20:20)
• isomorphism between sheaf F and Sheaftify of F.val (7 messages, latest: Jun 25 2025 at 08:50)
• Strong topology on linear maps (38 messages, latest: Jun 24 2025 at 08:50)
• Oriented Matroids (10 messages, latest: Jun 22 2025 at 03:59)
• Group-like elements and antipode (16 messages, latest: Jun 21 2025 at 13:44)
• category theory (471 messages, latest: Jun 19 2025 at 07:02)
• Category theory (1 message, latest: Jun 19 2025 at 05:55)
• Ramification Index equal to the card of inertia group (30 messages, latest: Jun 18 2025 at 15:10)
• Integral with respect to a complex measure (7 messages, latest: Jun 15 2025 at 10:48)
• Virasoro algebra (and cohomology of the Witt algebra) (14 messages, latest: Jun 15 2025 at 10:11)
• Extensional Equality for Recursively Defined Fuzzy Sets (79 messages, latest: Jun 14 2025 at 18:56)
• Definition of ordered rings (20 messages, latest: Jun 14 2025 at 17:32)
• Proving bijections in Lean (3 messages, latest: Jun 14 2025 at 14:57)
• preserving terminal objects at all universe levels (22 messages, latest: Jun 14 2025 at 11:24)
• List of blueprints (8 messages, latest: Jun 14 2025 at 04:44)
• PiLp complete space? (7 messages, latest: Jun 12 2025 at 22:14)
• what is an unramified extension? (32 messages, latest: Jun 11 2025 at 17:29)
• hasse derivative and homomorphism (2 messages, latest: Jun 10 2025 at 22:11)
• Monoids with non additive or multiplicative notation (28 messages, latest: Jun 10 2025 at 13:28)
• roots of unity - computing low degree (35 messages, latest: Jun 07 2025 at 20:23)
• Formalizing Probabilistic Arguments (7 messages, latest: Jun 07 2025 at 06:45)
• Discussion on formalization of Iwasawa Theory in Lean (14 messages, latest: Jun 05 2025 at 21:08)
• tendsto cofinite atTop (8 messages, latest: Jun 05 2025 at 00:40)
• Decidability on Rationals (5 messages, latest: Jun 03 2025 at 19:43)
• Product of Borel spaces (20 messages, latest: Jun 03 2025 at 08:20)
• Piecewise linear maps (17 messages, latest: Jun 02 2025 at 18:07)
• Uniform structures on ℝ (22 messages, latest: Jun 01 2025 at 16:10)
• Homotopy theory (1 message, latest: May 30 2025 at 13:28)
• restricted product puzzle (15 messages, latest: May 29 2025 at 19:14)
• JordanHolderLattice for Subgroup (13 messages, latest: May 28 2025 at 20:52)
• Low-dimensional Lie algebras (5 messages, latest: May 28 2025 at 02:41)
• Second Derivative Test (41 messages, latest: May 27 2025 at 18:14)
• Frucht's theorem without choice (17 messages, latest: May 27 2025 at 08:06)
• ring properties: local -> global (17 messages, latest: May 27 2025 at 08:06)
• Antilipschitz for linear maps (14 messages, latest: May 26 2025 at 19:39)
• Coalgebras/bialgebras/Hopf algebras (66 messages, latest: May 25 2025 at 21:21)
• actions on hom spaces (40 messages, latest: May 25 2025 at 16:42)
• (alternatingGroup (Fin 4))=⊤ (4 messages, latest: May 24 2025 at 14:40)
• walking arrow, walking isomorphism (3 messages, latest: May 23 2025 at 19:28)
• (Partial) Church's thesis (5 messages, latest: May 20 2025 at 12:46)
• Carneiro's thesis (transfer tactic not needed) (17 messages, latest: May 20 2025 at 05:09)
• ✔ Alexander subbasis theorem (21 messages, latest: May 15 2025 at 17:01)
• Open cells of a CW complex are open (8 messages, latest: May 13 2025 at 17:26)
• [How can I get 1/22=1 in Q[X?]](topic/How.20can.20I.20get.201.2F22.3D1.20in.20Q.5BX.3F.5D.html) (23 messages, latest: May 12 2025 at 18:25)
• instances for Rep R G (14 messages, latest: May 11 2025 at 17:07)
• Regret bound for online gradient descent (1 message, latest: May 09 2025 at 12:31)
• Compact open covered sets (11 messages, latest: May 07 2025 at 21:31)
• IsScalarTower maze (6 messages, latest: May 07 2025 at 15:55)
• Approximate a compact by a finite-dimensional compact (9 messages, latest: May 05 2025 at 20:48)
• Is this exercise in the book "The Mechanics of Proof" feasib (7 messages, latest: Apr 29 2025 at 10:08)
• Locally uniform convergence (21 messages, latest: Apr 28 2025 at 07:15)
• G-submodules (52 messages, latest: Apr 27 2025 at 18:11)
• A question about type mistakes (15 messages, latest: Apr 26 2025 at 20:10)
• How can I use the definition to prove this quetion? (4 messages, latest: Apr 26 2025 at 03:10)
• Natural equivalences and kernel performance (1 message, latest: Apr 23 2025 at 22:03)
• when is multiplication a monoid homomorphism? (8 messages, latest: Apr 21 2025 at 21:25)
• theorem direct_product_abelian_iff_factor_abelian (7 messages, latest: Apr 17 2025 at 18:12)
• definition of algebraic variety (56 messages, latest: Apr 17 2025 at 13:38)
• A statement about the center of a direct product (3 messages, latest: Apr 16 2025 at 15:01)
• On the uniqueness of solutions to congruential equations (16 messages, latest: Apr 16 2025 at 13:53)
• Infinite-dimensional manifolds (36 messages, latest: Apr 15 2025 at 21:35)
• CM-extensions of number fields (26 messages, latest: Apr 15 2025 at 08:39)
• Topology question (8 messages, latest: Apr 14 2025 at 21:04)
• Poincaré lemma (11 messages, latest: Apr 14 2025 at 20:52)
• Essential Injective Functors (8 messages, latest: Apr 12 2025 at 09:43)
• Fin.castSuccEmb and Fin.castLE (6 messages, latest: Apr 12 2025 at 06:18)
• ✔ Comultiplication is a hom when coalgebra is cocomm (14 messages, latest: Apr 09 2025 at 22:22)
• independent iff mul of laws equals laws of intersection (3 messages, latest: Apr 09 2025 at 10:50)
• ContinuousMul in a LinearOrderedSemifield? (4 messages, latest: Apr 09 2025 at 06:45)
• help with products in the category of types (15 messages, latest: Apr 08 2025 at 20:31)
• Taylor's theorem (49 messages, latest: Apr 07 2025 at 16:27)
• interesting, nonstandard explanation of quotient groups (53 messages, latest: Apr 07 2025 at 10:00)
• Parametric interval integrals (8 messages, latest: Apr 05 2025 at 13:21)
• Matrix simplification tactics (6 messages, latest: Apr 04 2025 at 19:33)
• Interesting examples of non-fibered prefibered cats? (5 messages, latest: Apr 03 2025 at 18:49)
• Easy simplification of linear equation (2 messages, latest: Mar 30 2025 at 17:34)
• The proposition 1.4 of hungerford algebra textbook. (9 messages, latest: Mar 30 2025 at 08:31)
• Ordered uniform spaces? (22 messages, latest: Mar 29 2025 at 08:57)
• Order adjoints and Galois connections (7 messages, latest: Mar 27 2025 at 00:07)
• Matrix type issue (32 messages, latest: Mar 24 2025 at 13:26)
• IsKFiltered.{k} ? (23 messages, latest: Mar 24 2025 at 03:17)
• commutative squares of isomorphisms (9 messages, latest: Mar 24 2025 at 00:50)
• Real-closed Hahn series (16 messages, latest: Mar 21 2025 at 23:16)
• Last step; Smoothness of vector bundle of alternating maps (15 messages, latest: Mar 21 2025 at 13:01)
• Proving product of two matrices (12 messages, latest: Mar 20 2025 at 17:49)
• ✔ Lifting Γ ⊣ Spec to the Over category (15 messages, latest: Mar 20 2025 at 17:02)
• colimits in Quiv.{v, u} (3 messages, latest: Mar 20 2025 at 00:38)
• Matrix theorem proof (25 messages, latest: Mar 17 2025 at 01:55)
• Showing that ↑a / ↑b = ↑(a / b) (6 messages, latest: Mar 15 2025 at 16:36)
• Abstract Simplicial Complex (17 messages, latest: Mar 14 2025 at 14:48)
• Inlining tests (23 messages, latest: Mar 13 2025 at 21:56)
• global sections functor (13 messages, latest: Mar 12 2025 at 17:38)
• Continuous functions on products (11 messages, latest: Mar 07 2025 at 22:26)
• ✔ commutative, idempotent semiring without zero? (25 messages, latest: Mar 07 2025 at 21:07)
• StrictMono for partial order (20 messages, latest: Mar 05 2025 at 10:13)
• Hölder triples (21 messages, latest: Mar 03 2025 at 17:44)
• Riemann zeta (11 messages, latest: Mar 03 2025 at 15:18)
• Separable extension of valuationSubring (6 messages, latest: Mar 01 2025 at 04:18)
• Tannaka duality for finite groups (14 messages, latest: Feb 28 2025 at 18:59)
• Uncountably long paths through a quiver (9 messages, latest: Feb 27 2025 at 02:24)
• PCF theory (56 messages, latest: Feb 26 2025 at 10:39)
• Is there an idiom for applying a subproof in two directions? (20 messages, latest: Feb 24 2025 at 09:03)
• Rewriting in slice categories (5 messages, latest: Feb 22 2025 at 05:10)
• {IsInducing,IsEmbedding}.sum_elim (20 messages, latest: Feb 21 2025 at 00:13)
• Proof of the LYM inequality using probability theory (10 messages, latest: Feb 18 2025 at 11:16)
• Commutative diagrams for diagram chasing (8 messages, latest: Feb 17 2025 at 12:55)
• Ordinal games (10 messages, latest: Feb 17 2025 at 10:44)
• dimension theory on noetherian local rings. (54 messages, latest: Feb 15 2025 at 01:38)
• Properties of wedge product of differential forms (8 messages, latest: Feb 14 2025 at 13:04)
• The nonmeasurability of the Vitali set (97 messages, latest: Feb 13 2025 at 22:34)
• Stokes' theorem (167 messages, latest: Feb 10 2025 at 11:30)
• ✔ How to show linearity of a map defined via tactics? (5 messages, latest: Feb 06 2025 at 21:14)
• Fibonacci (3 messages, latest: Feb 05 2025 at 06:47)
• Ideal of MvPolynomial of high degree (7 messages, latest: Feb 03 2025 at 20:19)
• all norms are equivalent on a fdvs over a complete field (13 messages, latest: Feb 02 2025 at 15:54)
• Reasoning about quotients (20 messages, latest: Jan 31 2025 at 09:41)
• Finitely supported restriction (23 messages, latest: Jan 31 2025 at 02:02)
• Nontrivial example of emetric space (12 messages, latest: Jan 30 2025 at 01:10)
• What to do about PGame (54 messages, latest: Jan 30 2025 at 00:24)
• Integral closure of ideals (4 messages, latest: Jan 29 2025 at 18:09)
• Poset games (179 messages, latest: Jan 28 2025 at 07:59)
• Help Needed: Proving Smoothness of a Bump Function in Lean (3 messages, latest: Jan 25 2025 at 06:42)
• ✔ A question about the use of definition of compactness (7 messages, latest: Jan 22 2025 at 15:44)
• Brunn-Minkowski Inequality + Theory (7 messages, latest: Jan 22 2025 at 13:56)
• MeasureSpace vs Measure in ProbabilityTheory/ (29 messages, latest: Jan 21 2025 at 14:17)
• Idle thoughts about module topology and adeles (4 messages, latest: Jan 20 2025 at 21:52)
• Sofa problem may have been solved (26 messages, latest: Jan 20 2025 at 02:24)
• Hodge star operator (87 messages, latest: Jan 18 2025 at 00:24)
• topology rational addition is continuous (4 messages, latest: Jan 17 2025 at 23:25)
• finite subgroup of group iso to Fˣ lies within finite field (21 messages, latest: Jan 16 2025 at 16:00)
• Limitation of ConvexOn Definition in mathlib4 (16 messages, latest: Jan 15 2025 at 13:39)
• Strength of Nonempty α → Squash α (34 messages, latest: Jan 14 2025 at 13:48)
• ✔ Is there a name for a "submodule" but w.r.t. a subring? (16 messages, latest: Jan 14 2025 at 02:24)
• Many possibilities for predual to d1 d0 - d0 d1 (2 messages, latest: Jan 13 2025 at 08:03)
• trace of endomorphism (16 messages, latest: Jan 12 2025 at 20:10)
• Convert smooth M → 𝕊ⁿ & M → ℝⁿ⁺¹ to smooth M → T𝕊ⁿ (7 messages, latest: Jan 11 2025 at 08:31)
• ✔ properties invariant under isomorphisms (12 messages, latest: Jan 09 2025 at 14:23)
• adic complete wrt a smaller ideal (8 messages, latest: Jan 08 2025 at 17:06)
• Free monoids in a monoidal category (5 messages, latest: Jan 08 2025 at 12:57)
• Generalizing normal functions (28 messages, latest: Jan 07 2025 at 07:03)
• ✔ The irrelevant ideal of R[n] (5 messages, latest: Jan 07 2025 at 03:17)
• Puzzles around finiteness and projectivity of modules (7 messages, latest: Jan 02 2025 at 14:53)
• Existence of a non-expanding linear projection (22 messages, latest: Dec 30 2024 at 23:57)
• An arbitrary choice that can only be made in one way (11 messages, latest: Dec 29 2024 at 21:54)
• ✔ Assistance Needed with Proving Properties of a Bump Fun… (2 messages, latest: Dec 26 2024 at 19:36)
• exists_rat_pow_btwn_rat without reals (31 messages, latest: Dec 26 2024 at 06:49)
• generalizing deriv to TVS (167 messages, latest: Dec 26 2024 at 03:20)
• ✔ Finishing off Jordan Normal Form for 2x2 matrices (4 messages, latest: Dec 26 2024 at 01:22)
• recommend intro to induction in vanilla lean4 (17 messages, latest: Dec 25 2024 at 05:57)
• Order Theory - POsets - a specific subset Definition (3 messages, latest: Dec 25 2024 at 05:51)
• Jacobi symbol (219 messages, latest: Dec 24 2024 at 20:26)
• Disjunction Normal Form for a generated boolean subalgebra (21 messages, latest: Dec 22 2024 at 18:08)
• ✔ Higher order arithmetic: Lean vs ZFC (5 messages, latest: Dec 21 2024 at 18:53)
• Computable Squash but noncomputable type? (15 messages, latest: Dec 20 2024 at 21:05)
• Disjoint subset in Boolean algebra? (5 messages, latest: Dec 19 2024 at 12:20)
• Recursive definition (8 messages, latest: Dec 19 2024 at 09:53)
• topology theorems for free via adjoint functors? (32 messages, latest: Dec 17 2024 at 19:43)
• Quantale (7 messages, latest: Dec 17 2024 at 14:38)
• ✔ Grothendieck universes, logical strength (7 messages, latest: Dec 16 2024 at 15:21)
• Dedekind Integers form a Ring (4 messages, latest: Dec 16 2024 at 14:25)
• LinearMap.det and restrictScalars (15 messages, latest: Dec 15 2024 at 15:34)
• Lebesgue density theorem, parametrized version (8 messages, latest: Dec 13 2024 at 13:32)
• Is this statement about filters true? (11 messages, latest: Dec 10 2024 at 20:35)
• Categories with an endomorphism functor (1 message, latest: Dec 09 2024 at 19:02)
• ✔ NontriviallyNormedField, CharP? (7 messages, latest: Dec 07 2024 at 22:34)
• Error with rewrite (18 messages, latest: Dec 05 2024 at 07:51)
• Proof help (8 messages, latest: Dec 04 2024 at 23:27)
• Levy hierarchy (8 messages, latest: Dec 04 2024 at 17:55)
• Refactor krullTopology? (22 messages, latest: Dec 04 2024 at 16:49)
• Cofinal sets (47 messages, latest: Dec 04 2024 at 11:27)
• How to define the set of all K-algebraic functions in Lean? (20 messages, latest: Dec 03 2024 at 22:43)
• Game relations (48 messages, latest: Dec 01 2024 at 23:16)
• Don't understand the definition of neighborhoods filter (12 messages, latest: Nov 30 2024 at 20:16)
• Induction on sum of geometric series (28 messages, latest: Nov 30 2024 at 15:07)
• Partial well-orders (17 messages, latest: Nov 30 2024 at 08:02)
• pushforward of tensor presheaves (11 messages, latest: Nov 29 2024 at 20:12)
• Does Schwartz-Zippel hold for Integral Domains? (19 messages, latest: Nov 28 2024 at 16:01)
• Notation for games (16 messages, latest: Nov 27 2024 at 18:54)
• product of pushforward topologies (41 messages, latest: Nov 27 2024 at 14:49)
• Relation between general cartesian product and prod (3 messages, latest: Nov 26 2024 at 14:08)
• generalized AM-GM (11 messages, latest: Nov 24 2024 at 21:30)
• Riesz representation theorem (47 messages, latest: Nov 24 2024 at 12:23)
• When can two types be compared using "="? (6 messages, latest: Nov 23 2024 at 04:44)
• Maximal abelian subgroup (13 messages, latest: Nov 22 2024 at 11:03)
• posterior distribution calculation (5 messages, latest: Nov 22 2024 at 06:11)
• Integral with values in LCTVS? (6 messages, latest: Nov 21 2024 at 07:58)
• Question about Subgroup.index (9 messages, latest: Nov 20 2024 at 19:40)
• "open Classical" vs "open scoped Classical" (2 messages, latest: Nov 20 2024 at 00:49)
• Multi-variable Fourier analysis (11 messages, latest: Nov 19 2024 at 22:07)
• the ring of integers corresponding to decomposition field (9 messages, latest: Nov 19 2024 at 16:47)
• ✔ Defining tensor product of (pre)sheaf of modules (7 messages, latest: Nov 17 2024 at 10:43)
• Why does "Finset a" require the assumption "DecidableEq a"? (54 messages, latest: Nov 16 2024 at 05:33)
• Path lifting (39 messages, latest: Nov 15 2024 at 07:42)
• challenges in the translation from a set proof to DTT? (55 messages, latest: Nov 12 2024 at 20:51)
• restricted products (16 messages, latest: Nov 12 2024 at 01:07)
• coordchange as function of base is smooth (5 messages, latest: Nov 05 2024 at 10:59)
• formalizing one point compactification (43 messages, latest: Nov 05 2024 at 07:40)
• Countability of inductive type (47 messages, latest: Nov 05 2024 at 00:15)
• p-adics manifolds with boundary? (10 messages, latest: Nov 04 2024 at 07:47)
• Ordinal notations (38 messages, latest: Nov 01 2024 at 03:45)
• Questions about ContinuousLinearMapWOT (7 messages, latest: Oct 30 2024 at 14:40)
• Does every type permit a semiring? (18 messages, latest: Oct 30 2024 at 10:12)
• Dependent type hell golfing challenge (24 messages, latest: Oct 29 2024 at 22:19)
• Center of General Linear Group (13 messages, latest: Oct 29 2024 at 10:17)
• Compactness of probability measures (7 messages, latest: Oct 28 2024 at 07:21)
• IsInaccesible definition (16 messages, latest: Oct 25 2024 at 20:46)
• Algebraic number theory (16 messages, latest: Oct 25 2024 at 15:50)
• A formal characterization of discrete condensed objects (4 messages, latest: Oct 24 2024 at 09:15)
• OEIS (17 messages, latest: Oct 22 2024 at 20:55)
• Formalising big results in functional analysis (5 messages, latest: Oct 22 2024 at 10:03)
• For measures, is MutuallySingular the same as Disjoint? (17 messages, latest: Oct 21 2024 at 13:23)
• "germ-injective" schemes (3 messages, latest: Oct 21 2024 at 12:42)
• Class number formula (34 messages, latest: Oct 21 2024 at 02:54)
• Inventiones Mathematica paper (3 messages, latest: Oct 16 2024 at 06:36)
• SeparableSpace (C(X, Y)) (27 messages, latest: Oct 16 2024 at 03:38)
• Ordinal.lsub (16 messages, latest: Oct 16 2024 at 00:13)
• Rectifiable paths (252 messages, latest: Oct 12 2024 at 18:43)
• FiniteMeasure vs IsFiniteMeasure (8 messages, latest: Oct 12 2024 at 14:10)
• Valuation rings that are not domains (15 messages, latest: Oct 11 2024 at 04:19)
• Question about Graded Stuff (11 messages, latest: Oct 10 2024 at 10:57)
• algebra puzzle (3 messages, latest: Oct 09 2024 at 00:33)
• The lattice of submodules (30 messages, latest: Oct 05 2024 at 23:09)
• Hypergeometric functions (19 messages, latest: Oct 05 2024 at 15:26)
• Error with rcases (5 messages, latest: Oct 04 2024 at 15:05)
• Improve a proof (4 messages, latest: Oct 03 2024 at 14:59)
• ((max)?gen)?{eigen,weight}space (18 messages, latest: Oct 03 2024 at 14:05)
• Definition for differential forms (36 messages, latest: Oct 03 2024 at 09:12)
• Introduce a class for Continuous DFunLike.coe? (17 messages, latest: Oct 03 2024 at 00:49)
• flt-regular (5 messages, latest: Oct 02 2024 at 14:21)
• Absolutely convex hull of a totally bounded set (3 messages, latest: Sep 30 2024 at 13:09)
• Naming: Typeclass (ULift α) ↔ Typeclass α (2 messages, latest: Sep 29 2024 at 00:56)
• CompleteSpace (E →SL[σ] F) (1 message, latest: Sep 29 2024 at 00:53)
• Divisors of a Natural Power (4 messages, latest: Sep 28 2024 at 06:20)
• Multiplicative version of NoZeroSMulDivisors? (7 messages, latest: Sep 26 2024 at 07:44)
• formalize proof of Catalan's conjecture or cyclotomic IMC? (6 messages, latest: Sep 25 2024 at 03:27)
• Idiomatic notation for interval comparison (7 messages, latest: Sep 24 2024 at 22:16)
• démonstartion (2 messages, latest: Sep 22 2024 at 11:01)
• Roots of meromorphic function on a connected set (40 messages, latest: Sep 21 2024 at 07:29)
• ✔ NoZeroSMulDivisors.Algebra.noZeroSMulDivisors (4 messages, latest: Sep 21 2024 at 01:34)
• Gödel's Incompleteness Theorem (9 messages, latest: Sep 20 2024 at 12:32)
• count_heartbeats bug? (13 messages, latest: Sep 20 2024 at 11:36)
• Cardinal.lift as an InitialSeg (17 messages, latest: Sep 20 2024 at 09:57)
• OuterMeasure constructors (2 messages, latest: Sep 19 2024 at 18:37)
• Heavy rfl (71 messages, latest: Sep 18 2024 at 00:00)
• Torus: quotient or pi? (33 messages, latest: Sep 17 2024 at 18:01)
• Order of the generator of a Finite Cyclic Group (6 messages, latest: Sep 15 2024 at 14:31)
• Ordinals as a ω-complete partial order (8 messages, latest: Sep 15 2024 at 03:29)
• ✔ prove existence of function extension (9 messages, latest: Sep 13 2024 at 16:56)
• Formalasing Alaoglu-Bourbaki theorem (4 messages, latest: Sep 12 2024 at 08:25)
• IsSuccLimit (44 messages, latest: Sep 12 2024 at 08:08)
• Well-founded recursion for pgames (910 messages, latest: Sep 11 2024 at 05:41)
• Lindemann-Weierstrass theorem almost done (66 messages, latest: Sep 10 2024 at 17:03)
• Isolated Zeros (11 messages, latest: Sep 10 2024 at 13:59)
• poly whose roots are the products of the roots of polys (11 messages, latest: Sep 09 2024 at 08:50)
• Groups with dense roots (9 messages, latest: Sep 08 2024 at 15:19)
• Minimum of Finset (4 messages, latest: Sep 08 2024 at 12:52)
• Doubts on definition of topologies (32 messages, latest: Sep 08 2024 at 12:41)
• Formalization of "chain of or" (15 messages, latest: Sep 07 2024 at 16:08)
• Kai-Kalai conjecture (14 messages, latest: Sep 07 2024 at 15:54)
• Dense submonoids vs subgroups (18 messages, latest: Sep 07 2024 at 15:48)
• Measure for some σ-algebra (5 messages, latest: Sep 02 2024 at 19:20)
• Formalising topological nets (58 messages, latest: Sep 01 2024 at 19:40)
• Still trying to grasp how far I should take formalizations (14 messages, latest: Aug 30 2024 at 03:21)
• Combinatorial maps (20 messages, latest: Aug 29 2024 at 20:52)
• ✔ Divisibility of Product implies Divisibility of Productees (4 messages, latest: Aug 29 2024 at 19:04)
• Completeness and compact convergence (17 messages, latest: Aug 29 2024 at 04:34)
• Conservative, ae (9 messages, latest: Aug 28 2024 at 22:03)
• Mechanics of Proof Exercise 5.3.6.3 (19 messages, latest: Aug 24 2024 at 20:57)
• Ordinal arithmetic via CNF (28 messages, latest: Aug 22 2024 at 23:48)
• ZF ordinal formalization (11 messages, latest: Aug 22 2024 at 21:45)
• Finsupp.lex backwards (8 messages, latest: Aug 22 2024 at 15:26)
• linear map to dual space (6 messages, latest: Aug 21 2024 at 11:11)
• Mechanics of Proof – Trouble rewriting factorial sometimes? (15 messages, latest: Aug 19 2024 at 22:57)
• Archimedean property in the reals (7 messages, latest: Aug 19 2024 at 09:44)
• Dyadic numbers (74 messages, latest: Aug 17 2024 at 20:17)
• Combinatorics / variant of Bell numbers (10 messages, latest: Aug 17 2024 at 10:41)
• Universal property of inclusion of principal filters (36 messages, latest: Aug 17 2024 at 09:46)
• covering space theory (4 messages, latest: Aug 16 2024 at 09:52)
• Birthday of game product (9 messages, latest: Aug 14 2024 at 01:37)
• Lovelier than a poem (2 messages, latest: Aug 13 2024 at 21:17)
• Transfinite recursion (7 messages, latest: Aug 13 2024 at 06:49)
• Game product cannot be lifted (15 messages, latest: Aug 13 2024 at 05:33)
• distributive law of monads (14 messages, latest: Aug 08 2024 at 13:37)
• Wandering points (7 messages, latest: Aug 07 2024 at 23:18)
• Pi of directed sets (4 messages, latest: Aug 07 2024 at 22:04)
• Defining a Type with multiple zeros (167 messages, latest: Aug 06 2024 at 14:00)
• ✔ Filter.Tendsto uniqueness (6 messages, latest: Aug 04 2024 at 01:29)
• Formalizing O(n lg n) efficient universal Turing macine (12 messages, latest: Aug 02 2024 at 14:47)
• span of linear forms (4 messages, latest: Aug 01 2024 at 17:53)
• Groups up to isomorphism (20 messages, latest: Jul 31 2024 at 06:37)
• Lebesgue conditional expectation (5 messages, latest: Jul 30 2024 at 13:37)
• Compactly generated spaces (43 messages, latest: Jul 27 2024 at 16:19)
• is dependent type theory a must to define a sheaf? (11 messages, latest: Jul 26 2024 at 16:20)
• Category of arrows and cartesian squares (5 messages, latest: Jul 26 2024 at 08:07)
• borel sigma-algebra & quotient topology (92 messages, latest: Jul 23 2024 at 09:58)
• offtopic: DecidableEq α implies #α ≤ ℵ₀? (10 messages, latest: Jul 22 2024 at 15:41)
• ergodic group actions (21 messages, latest: Jul 21 2024 at 15:57)
• ✔ Round function theorem (15 messages, latest: Jul 21 2024 at 02:18)
• Is Finset totally ordered? (16 messages, latest: Jul 20 2024 at 16:59)
• ✔ When is codiscrete not the bottom filter? (4 messages, latest: Jul 18 2024 at 09:23)
• ✔ LinearOrderedCommGroup on a subgroup (41 messages, latest: Jul 17 2024 at 07:59)
• Formalizing "Real Analysis" by Jay Cummings (5 messages, latest: Jul 17 2024 at 02:05)
• Nonarchimedean norms / ultrametric spaces in general (16 messages, latest: Jul 15 2024 at 14:45)
• Plane coloring problem formalization (2 messages, latest: Jul 15 2024 at 06:34)
• A question about getting a map (3 messages, latest: Jul 11 2024 at 08:52)
• Uses of Frobenius elements in mathematics (6 messages, latest: Jul 08 2024 at 08:54)
• Turing machines & gigantic numbers (40 messages, latest: Jul 06 2024 at 19:19)
• Categorical foundations of formalized condensed mathematics (8 messages, latest: Jul 05 2024 at 14:42)
• ✔ [help needed] How to eliminate nested ifs (14 messages, latest: Jul 05 2024 at 10:59)
• Naming for the setup of almost mathematics (8 messages, latest: Jul 04 2024 at 15:12)
• [help needed] how to synthesis the inner from TangentSpace (5 messages, latest: Jul 04 2024 at 07:19)
• exercise of the mechanics of proof (28 messages, latest: Jun 30 2024 at 22:02)
• Is the hierachy fixed? (1 message, latest: Jun 30 2024 at 21:53)
• Linear Algebra/Matrices: Elementary row operations, element (23 messages, latest: Jun 30 2024 at 15:01)
• heyting implication on Subobject X (7 messages, latest: Jun 29 2024 at 15:05)
• IsSeparable and Algebra.IsSeparable (8 messages, latest: Jun 28 2024 at 14:41)
• Surreal numbers (470 messages, latest: Jun 26 2024 at 10:01)
• Defining n-division polynomials (182 messages, latest: Jun 25 2024 at 14:19)
• T2 quotient (91 messages, latest: Jun 25 2024 at 01:57)
• Krasner's lemma (8 messages, latest: Jun 24 2024 at 15:23)
• how to specify an identity for a semigroup ? (11 messages, latest: Jun 23 2024 at 10:22)
• Formalizing stacks (69 messages, latest: Jun 22 2024 at 13:37)
• ✔ Condensed mathematics in Chinese (14 messages, latest: Jun 21 2024 at 16:41)
• making a topological ring (58 messages, latest: Jun 20 2024 at 18:01)
• How to fix this? (1 message, latest: Jun 20 2024 at 03:26)
• Ideal is intersection of comap_map along localisations (9 messages, latest: Jun 19 2024 at 21:32)
• Why types all the way up but not all the way down? (1 message, latest: Jun 19 2024 at 07:45)
• PosSMulMono and PosSMulStrictMono (9 messages, latest: Jun 18 2024 at 13:50)
• subsets (3 messages, latest: Jun 16 2024 at 20:51)
• A Universal Quantifier - thoughts (9 messages, latest: Jun 16 2024 at 10:11)
• Centralizer of centralizer of centralizer (26 messages, latest: Jun 10 2024 at 12:18)
• measurable_measure_prod_mk_left without s-finite (4 messages, latest: Jun 06 2024 at 10:03)
• #12978 and equality of objects (23 messages, latest: Jun 06 2024 at 08:34)
• Proving extensionality for category structure with 7 entries (12 messages, latest: Jun 03 2024 at 21:04)
• Vitali families (22 messages, latest: Jun 02 2024 at 20:17)
• Naming contest (73 messages, latest: Jun 01 2024 at 23:31)
• Gale-Shapley algorithm formalization (12 messages, latest: May 28 2024 at 23:10)
• ✔ Mechanics of Proof Exercise 2.5.9.8 (9 messages, latest: May 27 2024 at 20:34)
• nondegenerate bilinear form (13 messages, latest: May 27 2024 at 16:40)
• Tensor product and exact sequences (7 messages, latest: May 26 2024 at 16:50)
• sInf S ∈ S (8 messages, latest: May 23 2024 at 13:33)
• Choice and well-ordering (6 messages, latest: May 22 2024 at 22:42)
• McCoy's theorem (19 messages, latest: May 22 2024 at 10:53)
• Liouville's theorem for algebraic extensions (6 messages, latest: May 22 2024 at 01:34)
• kronecker symbol (18 messages, latest: May 19 2024 at 11:39)
• Lebesgue-Vitali for Riemann integrability (17 messages, latest: May 19 2024 at 06:02)
• Covering Space vs Covering Maps (15 messages, latest: May 17 2024 at 10:28)
• f = o(g) as a filter (9 messages, latest: May 17 2024 at 07:07)
• obtain topology from Borel σ-algebra? (7 messages, latest: May 17 2024 at 06:49)
• topology on tensor product (6 messages, latest: May 15 2024 at 05:55)
• Dedekind cuts and Well Founded Recursion (8 messages, latest: May 10 2024 at 07:44)
• proof fail? when the goal pops up as a condition (10 messages, latest: May 07 2024 at 14:56)
• The leanest proof of Zorn's Lemma (2 messages, latest: May 06 2024 at 14:29)
• a problem of reduction in lean4 (29 messages, latest: May 03 2024 at 16:35)
• Perfectoid spaces (3026 messages, latest: May 03 2024 at 02:53)
• Question regarding Pascal's triangle exercise in math2001 (1 message, latest: May 02 2024 at 01:03)
• Quantum algorithms for LWE (14 messages, latest: Apr 30 2024 at 17:03)
• Semicontinuity definition for non-linear orders (6 messages, latest: Apr 30 2024 at 10:40)
• 1-\epsilon method (10 messages, latest: Apr 29 2024 at 00:16)
• Confusing definition of filter pushforwards (28 messages, latest: Apr 26 2024 at 17:10)
• Rewriting vs. lifting (11 messages, latest: Apr 23 2024 at 22:45)
• Algebraic geometry (3 messages, latest: Apr 22 2024 at 22:50)
• ✔ help with setting up for mechanics of proofs course (3 messages, latest: Apr 21 2024 at 16:27)
• Weakening assumption of regular cardinal (12 messages, latest: Apr 20 2024 at 17:02)
• naming question: linear family of endoms (rank, regular) (6 messages, latest: Apr 20 2024 at 07:38)
• Quiver.opposite (3 messages, latest: Apr 19 2024 at 21:13)
• spectral theorem for normal endomorphisms and related pain (33 messages, latest: Apr 17 2024 at 19:36)
• Metrics on categories (16 messages, latest: Apr 16 2024 at 15:38)
• ERat as Semiring (56 messages, latest: Apr 16 2024 at 15:30)
• Glitch? (21 messages, latest: Apr 14 2024 at 21:50)
• Categorization of equivalence relations (18 messages, latest: Apr 13 2024 at 08:11)
• Much Less than Operator (26 messages, latest: Apr 11 2024 at 11:15)
• deprecated (3 messages, latest: Apr 10 2024 at 06:54)
• top space / manifold structure on points of alg varieties (37 messages, latest: Apr 08 2024 at 16:39)
• ValRingHom and ValAlgebra for valuations (23 messages, latest: Apr 01 2024 at 04:40)
• Properties of non-archimedean rings (22 messages, latest: Mar 31 2024 at 18:21)
• paper about Haar measure (36 messages, latest: Mar 30 2024 at 03:11)
• Mismatch between BSG in survey and LeanAPAP (20 messages, latest: Mar 27 2024 at 15:42)
• Uniform spaces, uniform add groups, and topological rings (10 messages, latest: Mar 25 2024 at 08:34)
• ✔ Interpreting asmyptotics notation (15 messages, latest: Mar 24 2024 at 23:12)
• sheafifying Kaehler differentials (30 messages, latest: Mar 24 2024 at 14:05)
• Generic faithfulness of the Burau representation (3 messages, latest: Mar 21 2024 at 09:00)
• Off topic (32 messages, latest: Mar 20 2024 at 14:13)
• Generating random theorems (7 messages, latest: Mar 19 2024 at 15:02)
• ✔ Giant linear algebra computation (9 messages, latest: Mar 17 2024 at 06:04)
• Formalizing Ramification Groups (7 messages, latest: Mar 16 2024 at 12:11)
• Covolume of a Z-lattice (23 messages, latest: Mar 16 2024 at 04:31)
• (combinatorial) surface classification theorem (23 messages, latest: Mar 13 2024 at 23:14)
• Continuity of AffineEquiv.constVAdd (6 messages, latest: Mar 13 2024 at 17:31)
• clean proof of Stone-Weierstrass analogue (30 messages, latest: Mar 13 2024 at 15:39)
• Practical ways to prove Nat.Prime N (7 messages, latest: Mar 12 2024 at 12:07)
• Discrete analysis (33 messages, latest: Mar 10 2024 at 16:30)
• contour integrals (6 messages, latest: Mar 09 2024 at 18:21)
• tensor product of bialgebras (55 messages, latest: Mar 07 2024 at 17:15)
• Continuity of convex functions (19 messages, latest: Mar 04 2024 at 12:59)
• difficulty with topology lemma and topological bases (3 messages, latest: Mar 01 2024 at 15:39)
• power series (147 messages, latest: Feb 29 2024 at 04:33)
• jordan-chevalley decomposition (52 messages, latest: Feb 28 2024 at 08:06)
• Specializing universal quantifier at elements of a subset (8 messages, latest: Feb 27 2024 at 18:08)
• How to define a set of functions satisfying some conditions (3 messages, latest: Feb 26 2024 at 18:55)
• Integrating function with values in LCS (1 message, latest: Feb 26 2024 at 14:00)
• Induction for a recursive function (3 messages, latest: Feb 25 2024 at 06:07)
• a closed subset of a closed subset is closed (type problems) (11 messages, latest: Feb 24 2024 at 20:05)
• Is there a name for "closure is the union of Specializes"? (45 messages, latest: Feb 24 2024 at 01:29)
• Continuous multilinear maps: assume Finite ι or not? (14 messages, latest: Feb 23 2024 at 19:18)
• ✔ Calc Proofs with some "dangling" added elements (17 messages, latest: Feb 18 2024 at 16:57)
• Setting up appropriate definitions for Lusin-Novikov (50 messages, latest: Feb 15 2024 at 17:56)
• Quadratic Maps (20 messages, latest: Feb 14 2024 at 18:29)
• Erdős–Ginzburg–Ziv theorem (14 messages, latest: Feb 11 2024 at 16:12)
• Witt's Cancellation (4 messages, latest: Feb 09 2024 at 05:53)
• An initial formalized Mandelbrot picture (4 messages, latest: Feb 08 2024 at 21:43)
• Probability space for infinite iid fair coin flips (10 messages, latest: Feb 08 2024 at 19:16)
• infer Module ℝ M from Module R M (10 messages, latest: Feb 08 2024 at 14:41)
• Density of Lipschitz continuous functions (12 messages, latest: Feb 02 2024 at 20:49)
• intersection of positive and positive definite cones? (8 messages, latest: Feb 01 2024 at 08:43)
• flat modules (114 messages, latest: Feb 01 2024 at 00:05)
• ✔ Triangle inequality arguments and bijecting from N x N … (14 messages, latest: Jan 29 2024 at 18:30)
• More Definitions and Theorems of Valuations (54 messages, latest: Jan 25 2024 at 13:17)
• CDGAs (121 messages, latest: Jan 24 2024 at 09:44)
• Q: The set of all elements of a type (12 messages, latest: Jan 23 2024 at 01:28)
• Support for cyclotomic units (23 messages, latest: Jan 21 2024 at 15:00)
• Definition of Absorbs (16 messages, latest: Jan 16 2024 at 21:13)
• ✔ LinearOrderedCancelAddCommMonoid with infima (16 messages, latest: Jan 16 2024 at 15:18)
• Star modules over non-commutative scalars (13 messages, latest: Jan 09 2024 at 01:01)
• Exponentials in seminormed algebras (45 messages, latest: Jan 06 2024 at 18:42)
• Sard's theorem (36 messages, latest: Jan 04 2024 at 15:43)
• finite_dimensional and finite (96 messages, latest: Jan 04 2024 at 14:19)
• ✔ Confusion using multiple classes (12 messages, latest: Jan 02 2024 at 01:46)
• ✔ Something like PFilter (5 messages, latest: Dec 27 2023 at 15:20)
• Vitali's convergence theorem (22 messages, latest: Dec 20 2023 at 12:59)
• ✔ Projectivization (36 messages, latest: Dec 20 2023 at 03:42)
• Hairer challenge (112 messages, latest: Dec 18 2023 at 10:03)
• Proving congruences by cases (30 messages, latest: Dec 15 2023 at 22:09)
• Cobordism hypothesis in 1-dimension. (6 messages, latest: Dec 14 2023 at 18:23)
• Partial converse to König's theorem (6 messages, latest: Dec 14 2023 at 11:31)
• Partial converse to König's lemma (1 message, latest: Dec 14 2023 at 10:42)
• Puzzle: noncommutative RingHom as typeclasses (10 messages, latest: Dec 14 2023 at 09:04)
• ✔ Comparing and indicator with a real (4 messages, latest: Dec 11 2023 at 22:36)
• commutative algebra status (10 messages, latest: Dec 10 2023 at 20:26)
• CounterExamples in Topology (10 messages, latest: Dec 09 2023 at 02:03)
• Trivial MeasurableSpaces (8 messages, latest: Dec 07 2023 at 20:31)
• ✔ I am confused (11 messages, latest: Dec 06 2023 at 07:48)
• An nth_simp_rw tactic would be great (3 messages, latest: Dec 01 2023 at 23:50)
• Formalizing a theoretical AI safety result (3 messages, latest: Nov 27 2023 at 12:06)
• Topology of enat (93 messages, latest: Nov 26 2023 at 18:21)
• Haar measures on affine spaces (8 messages, latest: Nov 24 2023 at 11:08)
• Universe trouble when using Module.Injective (20 messages, latest: Nov 23 2023 at 03:28)
• Set of quaternions that square to -1 (18 messages, latest: Nov 19 2023 at 19:38)
• infinity in positivity? (31 messages, latest: Nov 18 2023 at 00:53)
• Extensive Coverage (76 messages, latest: Nov 14 2023 at 08:40)
• x + x ≤ y + y → x ≤ y (36 messages, latest: Nov 12 2023 at 16:40)
• Proving a sum over smooth numbers is summable (34 messages, latest: Nov 12 2023 at 08:30)
• A recent proof about Ramsey numbers (20 messages, latest: Nov 08 2023 at 09:19)
• IsCoprime is @[simp]? (71 messages, latest: Nov 05 2023 at 18:48)
• Discrete correlation inequalities (22 messages, latest: Nov 03 2023 at 17:28)
• Tropically degree-bound polynomials (52 messages, latest: Nov 02 2023 at 16:02)
• Non-injective change of variables in integrals (31 messages, latest: Oct 30 2023 at 08:35)
• how do I say "a sentence is a theorem of a theory" in lean? (4 messages, latest: Oct 28 2023 at 17:50)
• Powers of ℤˣ by ZMod 2 (58 messages, latest: Oct 23 2023 at 18:55)
• Asymptotic series (5 messages, latest: Oct 23 2023 at 18:51)
• OrderedAddMonoid (11 messages, latest: Oct 22 2023 at 21:06)
• Hölder spaces (6 messages, latest: Oct 22 2023 at 15:06)
• submodules of a graded module (31 messages, latest: Oct 19 2023 at 13:13)
• How to actually compute midpoint (42 messages, latest: Oct 17 2023 at 15:28)
• Presieve of arrows for coproduct inclusions (4 messages, latest: Oct 16 2023 at 15:05)
• Three Whitehead theorems (10 messages, latest: Oct 16 2023 at 12:22)
• Tensor products of graded objects / chain complexes (34 messages, latest: Oct 16 2023 at 10:19)
• Mandelbrot - Lean 4 version (38 messages, latest: Oct 14 2023 at 19:23)
• Proofing convergence (15 messages, latest: Oct 14 2023 at 11:37)
• Monoidal instance on R-algebras (14 messages, latest: Oct 13 2023 at 15:53)
• ✔ Notation and context (7 messages, latest: Oct 13 2023 at 07:07)
• conjecture (8 messages, latest: Oct 12 2023 at 12:46)
• Hartogs's theorem (10 messages, latest: Oct 11 2023 at 19:57)
• Meromorphic functions (195 messages, latest: Oct 11 2023 at 19:55)
• ✔ ELan/Mathlib version compability (15 messages, latest: Oct 11 2023 at 11:38)
• Product of nonmeasurable sets (8 messages, latest: Oct 08 2023 at 23:50)
• New SAT result for a fragment of set theory (2 messages, latest: Oct 08 2023 at 07:13)
• Countable separating family of sets (3 messages, latest: Oct 07 2023 at 18:51)
• ae eq of preimages (20 messages, latest: Oct 06 2023 at 22:28)
• Finite projective planes of order 10 (10 messages, latest: Oct 06 2023 at 07:27)
• defining total complex (38 messages, latest: Oct 04 2023 at 09:12)
• MathLib installing (109 messages, latest: Oct 02 2023 at 08:06)
• How to define the Gaussian measure (19 messages, latest: Sep 29 2023 at 13:56)
• Alexandrov-discrete spaces (5 messages, latest: Sep 21 2023 at 10:32)
• Mandelbrot connectedness (19 messages, latest: Sep 20 2023 at 04:30)
• Bornology, topology (3 messages, latest: Sep 18 2023 at 05:43)
• Birkhoff ergodic theorem (11 messages, latest: Sep 17 2023 at 22:11)
• Pochhammer (11 messages, latest: Sep 16 2023 at 05:36)
• LinearOrderedSemiring (147 messages, latest: Sep 13 2023 at 10:55)
• notation for set of non-negative elements (10 messages, latest: Sep 12 2023 at 04:16)
• Eisenstein series (25 messages, latest: Sep 11 2023 at 23:40)
• σ-algebra of a.e-invariant sets (28 messages, latest: Sep 09 2023 at 20:43)
• Lean on Goldbach's conjecture (102 messages, latest: Sep 08 2023 at 23:41)
• module maps induced by ring homs (15 messages, latest: Sep 07 2023 at 17:44)
• polish implies second countable instance (15 messages, latest: Sep 06 2023 at 16:40)
• mod and lt (11 messages, latest: Sep 06 2023 at 08:33)
• Discriminant of a number field (64 messages, latest: Sep 05 2023 at 05:53)
• Blichfeldt's Theorem (3 messages, latest: Sep 04 2023 at 13:01)
• how to judge the common upper bound (2 messages, latest: Sep 01 2023 at 01:57)
• Euler factorization (8 messages, latest: Aug 30 2023 at 15:02)
• Perfect field (87 messages, latest: Aug 28 2023 at 20:55)
• stream events (2 messages, latest: Aug 22 2023 at 11:25)
• ring for semifields (5 messages, latest: Aug 20 2023 at 10:52)
• Introduce ℒp? (3 messages, latest: Aug 19 2023 at 17:18)
• proper maps (44 messages, latest: Aug 19 2023 at 08:12)
• Smooth manifolds (2 messages, latest: Aug 18 2023 at 23:37)
• [non-associative -algebras](topic/non-associative.20-algebras.html) (14 messages, latest: Aug 15 2023 at 03:16)
• Assumptions for continuity in Lp (13 messages, latest: Aug 14 2023 at 17:03)
• Model Theory - Is inv a function in the language of fields (7 messages, latest: Aug 14 2023 at 09:14)
• cast_subgroup_of_units_card_ne_zero for infinite fields (7 messages, latest: Aug 12 2023 at 22:05)
• ZeroAtInftyContinuousMap (12 messages, latest: Aug 12 2023 at 09:35)
• Model Theory - fields are field structures and vice versa (10 messages, latest: Aug 12 2023 at 02:44)
• Size of certain finset (23 messages, latest: Aug 10 2023 at 22:18)
• Partial order on FunLike (8 messages, latest: Aug 06 2023 at 21:09)
• LinearOrderedField with StarRing : TrivialStar (8 messages, latest: Aug 06 2023 at 16:08)
• sup_add / inf_add (1 message, latest: Aug 06 2023 at 01:22)
• Analytic structure groupoid (2 messages, latest: Aug 05 2023 at 17:32)
• definition of IsSeparable seems wrong for general rings (11 messages, latest: Aug 04 2023 at 10:23)
• Proving extentionality for category structure with 7 entries (22 messages, latest: Aug 03 2023 at 20:06)
• Int-equivariant equivs (36 messages, latest: Aug 01 2023 at 11:54)
• ✔ OfNat, Subtypes issues for ConvexCone.Pointed (39 messages, latest: Jul 31 2023 at 20:41)
• Coercion to/from Germ (2 messages, latest: Jul 31 2023 at 18:10)
• Typeclasses for ConvexCone (11 messages, latest: Jul 31 2023 at 15:21)
• UnivLE in CategoryTheory.Sites.SheafOfTypes ? (8 messages, latest: Jul 31 2023 at 12:53)
• linearly independent (4 messages, latest: Jul 30 2023 at 22:15)
• cardinality of prime numbers (6 messages, latest: Jul 29 2023 at 23:23)
• -1 raised to an integer (14 messages, latest: Jul 28 2023 at 16:05)
• Jets (19 messages, latest: Jul 27 2023 at 21:47)
• Minimal axioms for Group, CommRing etc (22 messages, latest: Jul 27 2023 at 20:06)
• Additive characters (51 messages, latest: Jul 27 2023 at 05:34)
• porting the sphere eversion project (19 messages, latest: Jul 26 2023 at 14:31)
• Diophantine approximation (97 messages, latest: Jul 25 2023 at 15:47)
• Perfect rings (3 messages, latest: Jul 25 2023 at 15:22)
• Is Finset directed? (20 messages, latest: Jul 23 2023 at 07:58)
• Representable natural transformations (1 message, latest: Jul 22 2023 at 10:49)
• time averages for ergodic theorems? (4 messages, latest: Jul 22 2023 at 05:46)
• type class for "Even" types? (11 messages, latest: Jul 22 2023 at 00:13)
• Use NeZero for measures? (19 messages, latest: Jul 21 2023 at 20:07)
• linarith failure (115 messages, latest: Jul 19 2023 at 19:42)
• convexity in the sphere eversion project (23 messages, latest: Jul 19 2023 at 12:46)
• Algebraic structure on Bool (20 messages, latest: Jul 17 2023 at 18:23)
• open CategoryTheory (21 messages, latest: Jul 17 2023 at 06:36)
• Finset of tuples with a given product (18 messages, latest: Jul 14 2023 at 13:34)
• Bounds on Pi with arbitrary precision (14 messages, latest: Jul 13 2023 at 23:14)
• Multiple topologies? (49 messages, latest: Jul 12 2023 at 14:15)
• affine space as a manifold (26 messages, latest: Jul 10 2023 at 05:51)
• Referencing hypothesis (4 messages, latest: Jul 10 2023 at 03:32)
• banach-steinhaus (9 messages, latest: Jul 06 2023 at 11:53)
• Beginnings of complex character theory (11 messages, latest: Jul 05 2023 at 06:19)
• !4#4871 positive elements in a star ordered ring (32 messages, latest: Jul 05 2023 at 00:41)
• ✔ Rename Memℒp? NO (7 messages, latest: Jul 04 2023 at 22:07)
• supremum is real or infinite (10 messages, latest: Jul 04 2023 at 06:27)
• Concrete categories (after port?) (7 messages, latest: Jul 03 2023 at 22:14)
• AlgebraicTopology.FundamentalGroupoid.Product (2 messages, latest: Jul 03 2023 at 21:38)
• 7 is prime? (16 messages, latest: Jul 03 2023 at 09:49)
• worries about is_R_or_C (46 messages, latest: Jul 02 2023 at 11:23)
• Schlessinger's criterion (9 messages, latest: Jul 01 2023 at 11:05)
• groups and rings in mathlib (9 messages, latest: Jun 30 2023 at 14:28)
• Fiber bundles (24 messages, latest: Jun 29 2023 at 15:44)
• Orthogonality in mathlib (31 messages, latest: Jun 28 2023 at 23:09)
• HasBinaryProduct vs HasFiniteProducts (9 messages, latest: Jun 27 2023 at 22:27)
• derivation (139 messages, latest: Jun 27 2023 at 13:59)
• Infinite sums of power series (18 messages, latest: Jun 26 2023 at 03:56)
• Sum of sum of ite simplifies to sum (7 messages, latest: Jun 23 2023 at 05:35)
• Action on functions (36 messages, latest: Jun 22 2023 at 17:01)
• maxHeartbeats bound (1 message, latest: Jun 21 2023 at 22:33)
• functor shapes (1 message, latest: Jun 21 2023 at 06:39)
• LFTCM2020 port (3 messages, latest: Jun 20 2023 at 20:50)
• ✔ Failed to synthesize instance (3 messages, latest: Jun 18 2023 at 12:34)
• Frames and frame homomorphisms (27 messages, latest: Jun 17 2023 at 18:25)
• Are CompleteDistribLattices completely distributive? (31 messages, latest: Jun 17 2023 at 05:12)
• Permission to push branch to mathlib (7 messages, latest: Jun 15 2023 at 20:38)
• Graded Modules (6 messages, latest: Jun 14 2023 at 23:05)
• ✔ fin.lean (14 messages, latest: Jun 14 2023 at 13:47)
• Advice about pushing PR to mathlib (21 messages, latest: Jun 14 2023 at 10:50)
• Diagonalisation (9 messages, latest: Jun 12 2023 at 06:00)
• New tactic for "relational congruence" (75 messages, latest: Jun 12 2023 at 05:09)
• ✔ ruesDiffSumOfRuesDiff help (7 messages, latest: Jun 11 2023 at 05:20)
• ✔ Diagonal sum simplification request. (28 messages, latest: Jun 10 2023 at 05:27)
• #9856 little wedderburn (50 messages, latest: Jun 08 2023 at 11:17)
• Topology on continuous_maps without a norm (43 messages, latest: Jun 07 2023 at 21:05)
• graphs edge_finset (8 messages, latest: Jun 06 2023 at 18:18)
• ✔ Resurrecting old mathlib code (19 messages, latest: Jun 04 2023 at 13:01)
• ✔ card on simple_graph (9 messages, latest: Jun 03 2023 at 14:39)
• about fderiv and the transformation of the types (5 messages, latest: Jun 02 2023 at 07:05)
• Universes of simplicial sets (26 messages, latest: Jun 01 2023 at 09:15)
• Banff videos (13 messages, latest: May 31 2023 at 20:57)
• Notation for linear_pmap (24 messages, latest: May 31 2023 at 14:31)
• lean-graded-rings-supersymmetry (6 messages, latest: May 31 2023 at 01:02)
• Seminar – London Learning Lean (9 messages, latest: May 29 2023 at 19:56)
• ✔ graph iso saves degree (10 messages, latest: May 28 2023 at 18:08)
• Structure sheaf of a complex manifold (13 messages, latest: May 26 2023 at 14:41)
• row rank equals column rank (7 messages, latest: May 25 2023 at 07:08)
• #19075 (16 messages, latest: May 24 2023 at 14:59)
• enough_projectives universe issue (3 messages, latest: May 22 2023 at 21:00)
• Wrong definition of residual? (8 messages, latest: May 19 2023 at 03:33)
• Measures on affine_space (5 messages, latest: May 18 2023 at 09:00)
• about fderiv and integral (9 messages, latest: May 18 2023 at 08:42)
• category theory documentation (57 messages, latest: May 17 2023 at 22:25)
• Binary Matrix Isomorphism (21 messages, latest: May 16 2023 at 17:01)
• Autogenerating parts of calcs (122 messages, latest: May 16 2023 at 15:51)
• Uglified proof (94 messages, latest: May 14 2023 at 09:18)
• Lean Infoview in Gitpod (33 messages, latest: May 11 2023 at 10:53)
• talk on tori (6 messages, latest: May 04 2023 at 17:56)
• left vs right modules in tensor products (240 messages, latest: May 04 2023 at 01:00)
• completion of uniform spaces (20 messages, latest: Apr 28 2023 at 13:47)
• a ∉ interior (Ici a) for partial orders (15 messages, latest: Apr 26 2023 at 16:14)
• DVRs (504 messages, latest: Apr 25 2023 at 17:56)
• The cyclotomic character (4 messages, latest: Apr 24 2023 at 08:24)
• Star ordered ring (83 messages, latest: Apr 23 2023 at 16:35)
• Cauchy sequences (47 messages, latest: Apr 19 2023 at 15:55)
• quotient norm group (6 messages, latest: Apr 18 2023 at 23:37)
• Absolute values & multiplicative ring norms (25 messages, latest: Apr 17 2023 at 09:47)
• floats vs. reals (6 messages, latest: Apr 15 2023 at 19:51)
• Coequilizers (6 messages, latest: Apr 15 2023 at 18:16)
• Map vector space to its double dual (18 messages, latest: Apr 15 2023 at 18:06)
• Can finite modules have non-finite rank, and vice versa? (22 messages, latest: Apr 14 2023 at 09:43)
• Additive characters on topological fields (11 messages, latest: Apr 10 2023 at 17:49)
• finite cyclic structure (6 messages, latest: Apr 09 2023 at 16:19)
• well_founded.min (25 messages, latest: Apr 07 2023 at 07:18)
• Simply connected complements in the sphere (6 messages, latest: Apr 05 2023 at 13:58)
• Pythagorean Theorem With Trig (10 messages, latest: Apr 04 2023 at 15:14)
• Continuity of bilinear maps (11 messages, latest: Apr 03 2023 at 21:56)
• definition of doubling measures (27 messages, latest: Mar 31 2023 at 18:47)
• New linear algebra notation (59 messages, latest: Mar 31 2023 at 08:19)
• Smooth vector bundles (28 messages, latest: Mar 31 2023 at 05:42)
• ZFC hom renames (49 messages, latest: Mar 30 2023 at 13:19)
• Small initial segments (7 messages, latest: Mar 29 2023 at 07:55)
• Using classes of linear_map (10 messages, latest: Mar 27 2023 at 21:54)
• ✔ Is the zero algebra normed? (45 messages, latest: Mar 27 2023 at 18:20)
• ✔ Nat- and Int-modules homomorphisms (5 messages, latest: Mar 27 2023 at 09:50)
• trouble in shift_functor land (71 messages, latest: Mar 27 2023 at 08:46)
• partial derivatives (82 messages, latest: Mar 26 2023 at 16:52)
• dimension of a ring / topological space (40 messages, latest: Mar 26 2023 at 15:17)
• picking up lean4 with math (24 messages, latest: Mar 26 2023 at 09:39)
• An Aperiodic Monotile (19 messages, latest: Mar 25 2023 at 03:07)
• ✔ lim 1/n (6 messages, latest: Mar 25 2023 at 00:35)
• jordan normal form (23 messages, latest: Mar 19 2023 at 17:28)
• inner_product_space and normed_algebra (13 messages, latest: Mar 17 2023 at 22:32)
• Exponential Banach Algebra (35 messages, latest: Mar 17 2023 at 21:12)
• is_hermitian vs is_self_adjoint (27 messages, latest: Mar 16 2023 at 20:02)
• SVD (53 messages, latest: Mar 15 2023 at 13:00)
• ✔ Complex differentiable_at, complex polynomials , lift abs (19 messages, latest: Mar 14 2023 at 18:34)
• Open determinacy (29 messages, latest: Mar 13 2023 at 19:05)
• internal/external direct sum (12 messages, latest: Mar 13 2023 at 15:04)
• parametrised curves (20 messages, latest: Mar 10 2023 at 03:27)
• Solid (49 messages, latest: Mar 08 2023 at 15:18)
• Second grade student (4 messages, latest: Mar 08 2023 at 15:16)
• Restriction of open set to subtype topology (10 messages, latest: Mar 07 2023 at 03:10)
• Defining initial ordinals (16 messages, latest: Mar 06 2023 at 20:16)
• Induction principle for well-founded recursion definition (3 messages, latest: Mar 06 2023 at 10:01)
• associativity tactic (9 messages, latest: Mar 05 2023 at 23:06)
• topology on units (24 messages, latest: Mar 03 2023 at 10:19)
• Algebraic geometry development (136 messages, latest: Mar 02 2023 at 16:01)
• noetherian modules (96 messages, latest: Mar 02 2023 at 13:43)
• hereditarily (41 messages, latest: Mar 01 2023 at 11:27)
• Geach-Kaplan sentence (3 messages, latest: Feb 28 2023 at 00:21)
• A bijective prefunctor has an inverse:  eq.rec goal (20 messages, latest: Feb 27 2023 at 14:10)
• prove basic things. (3 messages, latest: Feb 26 2023 at 19:04)
• Dirichlet's unit theorem (18 messages, latest: Feb 24 2023 at 14:31)
• Several questions about constants (12 messages, latest: Feb 24 2023 at 09:42)
• Slow proofs in group_cohomology_resolution (6 messages, latest: Feb 23 2023 at 23:17)
• Timeout using particular ring hom in general universe (2 messages, latest: Feb 23 2023 at 05:35)
• normed_field (32 messages, latest: Feb 21 2023 at 23:40)
• lawvere theories (23 messages, latest: Feb 21 2023 at 20:47)
• noisy ring (16 messages, latest: Feb 21 2023 at 00:50)
• Klein's Vierergruppe, and conjugacy classes (33 messages, latest: Feb 16 2023 at 20:45)
• documentation on metric spaces (2 messages, latest: Feb 15 2023 at 23:17)
• literals in int (9 messages, latest: Feb 13 2023 at 11:28)
• documentation on the unit interval and metric spaces (5 messages, latest: Feb 13 2023 at 09:33)
• homotopy theory (31 messages, latest: Feb 12 2023 at 22:27)
• opens.map and opens.comap (4 messages, latest: Feb 10 2023 at 14:39)
• ZFC pair rename (29 messages, latest: Feb 04 2023 at 17:55)
• quotient inconsistency (2 messages, latest: Jan 30 2023 at 22:14)
• don't know how to synthesize placeholder (11 messages, latest: Jan 30 2023 at 21:53)
• Quasi-finite locus under base change (1 message, latest: Jan 26 2023 at 18:46)
• ZFC image (15 messages, latest: Jan 24 2023 at 04:08)
• Domain theory (3 messages, latest: Jan 20 2023 at 14:52)
• nat_abs less or equal (4 messages, latest: Jan 16 2023 at 10:29)
• Muirhead's inequality (5 messages, latest: Jan 15 2023 at 21:45)
• Mod 2 alternating truth value (11 messages, latest: Jan 13 2023 at 12:07)
• Linear algebra (15 messages, latest: Jan 12 2023 at 20:20)
• Set intervals names (43 messages, latest: Jan 12 2023 at 16:53)
• riemannian geometry (13 messages, latest: Jan 12 2023 at 16:24)
• Type checker runs out of memory (22 messages, latest: Jan 12 2023 at 15:15)
• Help wanted: infinite sums over Z (2 messages, latest: Jan 12 2023 at 09:38)
• analytical number theory (67 messages, latest: Jan 11 2023 at 15:07)
• define polynomials recursively (9 messages, latest: Jan 11 2023 at 11:31)
• Currying in tsum_prod definition (5 messages, latest: Jan 10 2023 at 16:14)
• hyperoperation rw not rewriting properly (12 messages, latest: Jan 10 2023 at 04:07)
• No more PRs? (30 messages, latest: Jan 09 2023 at 13:45)
• Kneser's addition theorem (9 messages, latest: Jan 09 2023 at 13:09)
• help proving properties about subsets of N (10 messages, latest: Jan 08 2023 at 20:39)
• Group filter bases (11 messages, latest: Jan 08 2023 at 19:34)
• computing degrees of polynomials (3 messages, latest: Jan 07 2023 at 17:21)
• Using option to define operators (12 messages, latest: Jan 03 2023 at 16:47)
• 1 ≤ 1 = true (11 messages, latest: Jan 02 2023 at 21:02)
• Alternative to mono? (11 messages, latest: Jan 02 2023 at 21:01)
• Hartog's theorem (15 messages, latest: Jan 02 2023 at 19:55)
• Unitary representation (2 messages, latest: Jan 02 2023 at 02:57)
• Abelianization (3 messages, latest: Jan 01 2023 at 00:29)
• linear_pmap (5 messages, latest: Dec 31 2022 at 22:53)
• Montel's theorem (65 messages, latest: Dec 26 2022 at 23:53)
• Star semiring (13 messages, latest: Dec 22 2022 at 17:18)
• quiz: course-of-values recursion (4 messages, latest: Dec 22 2022 at 11:07)
• Order of product of commuting elements of a group (14 messages, latest: Dec 22 2022 at 04:48)
• a characterization of real.exp (3 messages, latest: Dec 21 2022 at 07:36)
• ✔ class_group.mk (1 message, latest: Dec 19 2022 at 16:36)
• Why is class_group.mk so slow? (16 messages, latest: Dec 19 2022 at 14:06)
• Triple products in statements (2 messages, latest: Dec 18 2022 at 07:58)
• Iwasawa Criterion for simplicity (23 messages, latest: Dec 17 2022 at 14:29)
• Degrees of polynomials in many variables (14 messages, latest: Dec 16 2022 at 17:45)
• ✔ using cardinality for existence proof (4 messages, latest: Dec 16 2022 at 04:29)
• using cardinality for existence proof (1 message, latest: Dec 16 2022 at 01:41)
• ✔ Mathlib installation on Linux (2 messages, latest: Dec 12 2022 at 19:04)
• Mathlib installation on Linux (6 messages, latest: Dec 12 2022 at 16:59)
• Properties on fintype_inverse_systems (12 messages, latest: Dec 12 2022 at 10:28)
• Borel hierarchy (49 messages, latest: Dec 11 2022 at 21:21)
• ✔ subtraction canceling on natural numbers (7 messages, latest: Dec 09 2022 at 17:45)
• Does metric_space really belong in topology ? (6 messages, latest: Dec 09 2022 at 07:23)
• tendsto_log (6 messages, latest: Dec 07 2022 at 17:34)
• unfold notations used in set theory (5 messages, latest: Dec 05 2022 at 22:33)
• Bimonoids (3 messages, latest: Dec 02 2022 at 13:50)
• ✔ Dihedral group element composition definitions (1 message, latest: Dec 01 2022 at 09:36)
• Dihedral group element composition definitions (24 messages, latest: Nov 30 2022 at 22:54)
• sampling a pmf (12 messages, latest: Nov 30 2022 at 19:17)
• ereal multiplication (16 messages, latest: Nov 30 2022 at 10:33)
• argmin (4 messages, latest: Nov 30 2022 at 08:50)
• ennreal multiplication (5 messages, latest: Nov 29 2022 at 10:56)
• morphism in (topological_space.opens X)ᵒᵖ (11 messages, latest: Nov 28 2022 at 19:22)
• EPSRC TCC algebraic geometry course (1 message, latest: Nov 26 2022 at 00:15)
• category_theory.Sheaf.category_theory (1 message, latest: Nov 25 2022 at 23:45)
• Sphere eversion project (309 messages, latest: Nov 23 2022 at 09:29)
• ✔ Where does left_cancel_semigroup fit into the hierarchy (2 messages, latest: Nov 22 2022 at 21:25)
• Where does left_cancel_semigroup fit into the hierarchy (5 messages, latest: Nov 22 2022 at 21:00)
• Cantor-Bendixson (39 messages, latest: Nov 22 2022 at 08:20)
• github access (28 messages, latest: Nov 19 2022 at 21:41)
• bilinear_form (36 messages, latest: Nov 18 2022 at 22:28)
• Halving inequaities (22 messages, latest: Nov 17 2022 at 10:58)
• ✔ Failing to resolve imports after upgrading mathlib (31 messages, latest: Nov 16 2022 at 22:30)
• Failing to resolve imports after upgrading mathlib (1 message, latest: Nov 16 2022 at 22:00)
• ✔ mathlib permission? (4 messages, latest: Nov 16 2022 at 03:22)
• mathlib permission? (3 messages, latest: Nov 16 2022 at 02:22)
• Why is eq more important than heq? (42 messages, latest: Nov 15 2022 at 17:57)
• construction of some basic things (beginner question) (2 messages, latest: Nov 15 2022 at 02:25)
• large numbers computations (74 messages, latest: Nov 10 2022 at 13:46)
• Seminorm balls (12 messages, latest: Nov 10 2022 at 11:25)
• how do I factor a polynomial in lean 3? (11 messages, latest: Nov 10 2022 at 05:57)
• is_central_vadd (1 message, latest: Nov 09 2022 at 00:56)
• Jordan Hölder theorem (45 messages, latest: Nov 08 2022 at 18:59)
• nnreal vs. ennreal in pmf (12 messages, latest: Nov 08 2022 at 01:03)
• measurable Cantor-Schroeder-Bernstein (12 messages, latest: Nov 03 2022 at 17:52)
• Convex functions are continuous (20 messages, latest: Nov 02 2022 at 17:13)
• Notation for ext_chart_at (10 messages, latest: Nov 02 2022 at 10:16)
• ✔ Evaluating multivariable functions (2 messages, latest: Nov 02 2022 at 01:22)
• Evaluating multivariable functions (22 messages, latest: Nov 02 2022 at 01:21)
• ✔ Step out of Anonymous Constructors? (5 messages, latest: Nov 01 2022 at 19:04)
• ✔ Free semigroups, finiteness, and finite generation (13 messages, latest: Nov 01 2022 at 16:18)
• ✔ Unfold Multiplication in Group (5 messages, latest: Nov 01 2022 at 02:23)
• Unfold Multiplication in Group (1 message, latest: Nov 01 2022 at 01:22)
• nonconstructive type finiteness (3 messages, latest: Oct 30 2022 at 22:28)
• refl won't prove J <= J for ideals (31 messages, latest: Oct 30 2022 at 19:56)
• Compatibility of topology and order without algebra (6 messages, latest: Oct 28 2022 at 21:56)
• The category of sheaves is balanced. (5 messages, latest: Oct 28 2022 at 06:28)
• Prove Quotient is initial (2 messages, latest: Oct 26 2022 at 12:43)
• Distribution theory (78 messages, latest: Oct 26 2022 at 07:27)
• ✔ project doesn't accept mathlib oleans (20 messages, latest: Oct 25 2022 at 20:34)
• integral curves on manifold (2 messages, latest: Oct 24 2022 at 23:57)
• project doesn't accept mathlib oleans (31 messages, latest: Oct 24 2022 at 11:18)
• Infinite Fermat pseudoprimes to any base (15 messages, latest: Oct 23 2022 at 12:35)
• free filters and ultrafilters (35 messages, latest: Oct 22 2022 at 17:10)
• Geometric group theory (132 messages, latest: Oct 20 2022 at 09:59)
• Calculus on the circle (5 messages, latest: Oct 19 2022 at 17:31)
• ✔ destructuring products (16 messages, latest: Oct 19 2022 at 16:00)
• ✔ Commuting sum sigmas with a sum of sum of sum (3 messages, latest: Oct 18 2022 at 02:21)
• Normed groups conflict (10 messages, latest: Oct 17 2022 at 22:16)
• Commuting sum sigmas with a sum of sum of sum (5 messages, latest: Oct 17 2022 at 21:14)
• difference of floors (7 messages, latest: Oct 17 2022 at 11:37)
• Algebraic topology (8 messages, latest: Oct 16 2022 at 14:43)
• empty set lemmas (3 messages, latest: Oct 16 2022 at 08:25)
• equiv.perm : card of centralizers and of conjugacy classes (1 message, latest: Oct 15 2022 at 11:54)
• ring_hom_class woes (5 messages, latest: Oct 15 2022 at 06:56)
• Set predicates and set-like. (4 messages, latest: Oct 14 2022 at 17:58)
• Order-connected sets are measurable (31 messages, latest: Oct 14 2022 at 16:30)
• Lagrange multipliers (1 message, latest: Oct 14 2022 at 14:15)
• docs#metric.diam vs docs#emetric.diam (9 messages, latest: Oct 14 2022 at 14:01)
• Fermat Last Theorem for regular primes (109 messages, latest: Oct 14 2022 at 00:54)
• Refactoring ring spectra (5 messages, latest: Oct 12 2022 at 14:14)
• ✔ gcd_monoid (10 messages, latest: Oct 12 2022 at 02:27)
• gcd_monoid (27 messages, latest: Oct 11 2022 at 22:03)
• ✔ rw not working when it obviously should (1 message, latest: Oct 11 2022 at 10:20)
• rw not working when it obviously should (21 messages, latest: Oct 11 2022 at 06:29)
• category_theory.quotient type synonym? (6 messages, latest: Oct 10 2022 at 07:40)
• Formalizing theorems using Lean4 (17 messages, latest: Oct 09 2022 at 15:48)
• A function that is a sum of said function (41 messages, latest: Oct 08 2022 at 17:23)
• ✔ f = g implies deriv f = deriv g (1 message, latest: Oct 08 2022 at 14:23)
• f = g implies deriv f = deriv g (6 messages, latest: Oct 08 2022 at 14:02)
• ✔ S-integers and S-units (1 message, latest: Oct 07 2022 at 04:15)
• ✔ Selmer groups of number fields (1 message, latest: Oct 07 2022 at 04:14)
• ring_mul_action (27 messages, latest: Oct 06 2022 at 16:32)
• Completable top field (9 messages, latest: Oct 04 2022 at 20:17)
• Logic Question (3 messages, latest: Oct 02 2022 at 00:23)
• Existence of a recursor (2 messages, latest: Oct 01 2022 at 19:53)
• Multinomial formula (1 message, latest: Oct 01 2022 at 17:25)
• H-spaces (1 message, latest: Sep 30 2022 at 23:01)
• ✔ Having trouble taking a derivative (1 message, latest: Sep 30 2022 at 22:04)
• ✔ Introduce proof that is member of structure? (19 messages, latest: Sep 30 2022 at 21:47)
• Having trouble taking a derivative (37 messages, latest: Sep 30 2022 at 11:28)
• Internal categories (12 messages, latest: Sep 29 2022 at 19:47)
• norm_cast trace (4 messages, latest: Sep 28 2022 at 15:42)
• Construction of structures (13 messages, latest: Sep 26 2022 at 13:38)
• Category Type (10 messages, latest: Sep 23 2022 at 20:10)
• submodule induction (11 messages, latest: Sep 23 2022 at 16:18)
• Hypotheses/conclusions for strictly positive natural numbers (33 messages, latest: Sep 23 2022 at 08:45)
• Help {generalize, rename} these lemmas for mathlib (18 messages, latest: Sep 22 2022 at 20:41)
• Showing a sum is summable (21 messages, latest: Sep 22 2022 at 19:13)
• Fourier transform (17 messages, latest: Sep 20 2022 at 15:01)
• finite choice / surjectivity of Pi-terms (20 messages, latest: Sep 20 2022 at 09:31)
• What's this typeclass? (49 messages, latest: Sep 19 2022 at 15:55)
• product families of groups (12 messages, latest: Sep 19 2022 at 15:07)
• Philosophical questions about equality (13 messages, latest: Sep 18 2022 at 13:16)
• constructive (computable) power rule (8 messages, latest: Sep 16 2022 at 21:27)
• Birthday problem (22 messages, latest: Sep 16 2022 at 13:56)
• Path metric (1 message, latest: Sep 15 2022 at 08:38)
• Categories where coproduct injections are mono (3 messages, latest: Sep 15 2022 at 07:16)
• limits in opposite categories (6 messages, latest: Sep 14 2022 at 23:19)
• Misc semigroup stuff (12 messages, latest: Sep 13 2022 at 21:35)
• permutations : of_subtype vs extend_domain (5 messages, latest: Sep 12 2022 at 17:24)
• ZFC's properties (12 messages, latest: Sep 11 2022 at 16:49)
• Dimensional Analysis Community Input (45 messages, latest: Sep 10 2022 at 23:49)
• Euclidean challenge (9 messages, latest: Sep 09 2022 at 16:14)
• Subtype of a measure space (15 messages, latest: Sep 09 2022 at 12:19)
• A couple of easy PRs (1 message, latest: Sep 09 2022 at 09:59)
• Convex bodies (32 messages, latest: Sep 08 2022 at 10:12)
• Graded ring of modular forms (24 messages, latest: Sep 07 2022 at 23:47)
• second order logic (1 message, latest: Sep 06 2022 at 07:02)
• TC for pointwise operations on fun_like? (6 messages, latest: Sep 05 2022 at 07:37)
• Unitary is not linear? (12 messages, latest: Sep 04 2022 at 04:54)
• Empty torsors (15 messages, latest: Sep 03 2022 at 06:43)
• ✔ Unitary is not linear? (3 messages, latest: Sep 02 2022 at 01:42)
• hermite polynomials (21 messages, latest: Sep 01 2022 at 17:36)
• Algorithm for intuitionistic propositional logic (6 messages, latest: Sep 01 2022 at 15:22)
• Parity lemmas for natural numbers (11 messages, latest: Aug 31 2022 at 17:30)
• Karamata's inequality (2 messages, latest: Aug 30 2022 at 08:45)
• How can do "rcases" on a (not computable?) exists statement (5 messages, latest: Aug 30 2022 at 03:19)
• Adjunction formula WIP blueprint (2 messages, latest: Aug 27 2022 at 09:28)
• S-integers and S-units (39 messages, latest: Aug 26 2022 at 22:58)
• Adjunction forula WIP blueprint (1 message, latest: Aug 26 2022 at 22:27)
• Ordered monoids (11 messages, latest: Aug 25 2022 at 11:37)
• docs#ordered_smul (7 messages, latest: Aug 25 2022 at 08:07)
• Heights on rational elliptic curves (1 message, latest: Aug 24 2022 at 22:41)
• Young tableaux and RSK (39 messages, latest: Aug 24 2022 at 21:30)
• equiv_like extending fun_like (71 messages, latest: Aug 24 2022 at 13:12)
• Feedback wanted on Hamming implementation (50 messages, latest: Aug 24 2022 at 06:53)
• Opposite of diameter of an (e)metric space. (56 messages, latest: Aug 24 2022 at 01:29)
• linear_pmap_class (21 messages, latest: Aug 23 2022 at 00:39)
• Convex join (10 messages, latest: Aug 21 2022 at 05:42)
• how to define positive cones in $\mathbb{R}^n$? (35 messages, latest: Aug 19 2022 at 13:57)
• lie_ring.to_non_unital_non_assoc_semiring (8 messages, latest: Aug 19 2022 at 13:43)
• matrix.minor wrong terminology? (19 messages, latest: Aug 18 2022 at 13:38)
• "The" Riemann-Roch theorem (29 messages, latest: Aug 17 2022 at 19:30)
• division_monoid and is_unit (35 messages, latest: Aug 17 2022 at 18:58)
• ideals in non-comm rings (339 messages, latest: Aug 16 2022 at 18:53)
• nonconstructive polynomials (20 messages, latest: Aug 15 2022 at 10:49)
• ✔ Resolvent set for linear_pmap (2 messages, latest: Aug 15 2022 at 09:21)
• Resolvent set for linear_pmap (1 message, latest: Aug 15 2022 at 09:04)
• ✔ using adjoint of a continuous linear map (12 messages, latest: Aug 13 2022 at 18:46)
• Kakeya problem (21 messages, latest: Aug 11 2022 at 16:37)
• Definition of compactness using filter (11 messages, latest: Aug 11 2022 at 13:18)
• equivalence between ℓp and Lp (14 messages, latest: Aug 11 2022 at 07:43)
• dagger categories (28 messages, latest: Aug 11 2022 at 00:58)
• prod of inner product spaces (33 messages, latest: Aug 10 2022 at 21:22)
• hypotheses for a field property (57 messages, latest: Aug 10 2022 at 20:16)
• Missing facts about locally_constant (11 messages, latest: Aug 09 2022 at 20:03)
• checking cases in zmod 4 (9 messages, latest: Aug 09 2022 at 18:40)
• Gauss sums (50 messages, latest: Aug 09 2022 at 15:56)
• Iterated_fderiv lemmas (22 messages, latest: Aug 07 2022 at 09:44)
• Directional words in nomenclature? (22 messages, latest: Aug 06 2022 at 05:23)
• Objects with no canonical definition (15 messages, latest: Aug 05 2022 at 09:03)
• set.nontrivial (33 messages, latest: Aug 05 2022 at 00:34)
• Newton's identities (10 messages, latest: Aug 04 2022 at 16:28)
• chebyshev polynomials (47 messages, latest: Aug 03 2022 at 08:37)
• first_order.language.sum (1 message, latest: Aug 02 2022 at 01:24)
• Monoidal composition (10 messages, latest: Aug 01 2022 at 19:53)
• Defining proper (convex) cones (1 message, latest: Aug 01 2022 at 18:37)
• Renaming normed_group (25 messages, latest: Aug 01 2022 at 13:04)
• How to add a path exactly (6 messages, latest: Jul 31 2022 at 08:55)
• Using the LTE snake lemma (70 messages, latest: Jul 30 2022 at 17:48)
• Reconstructing a filter from its points (8 messages, latest: Jul 30 2022 at 02:50)
• radon measures (10 messages, latest: Jul 28 2022 at 05:09)
• Positive operators (21 messages, latest: Jul 27 2022 at 19:14)
• disjoint decomposition (11 messages, latest: Jul 27 2022 at 11:18)
• Generalisation of "even part" and "odd part"? (31 messages, latest: Jul 27 2022 at 05:38)
• Subrepresentations (36 messages, latest: Jul 26 2022 at 09:39)
• Kahler differentials (41 messages, latest: Jul 26 2022 at 07:46)
• Old docs (3 messages, latest: Jul 25 2022 at 20:14)
• removable singularity (7 messages, latest: Jul 24 2022 at 21:16)
• CPTP maps on Hilbert spaces (11 messages, latest: Jul 24 2022 at 18:37)
• Comparison in preorders (24 messages, latest: Jul 24 2022 at 18:18)
• succ_order and pred_order design (120 messages, latest: Jul 24 2022 at 14:10)
• The cardinal #(Type u) (21 messages, latest: Jul 24 2022 at 10:47)
• The bicategory of algebras and bimodules (43 messages, latest: Jul 24 2022 at 03:44)
• algebra_map as coercion, and norm_cast (7 messages, latest: Jul 22 2022 at 19:04)
• Group cohomology (54 messages, latest: Jul 22 2022 at 13:05)
• (no topic) (6 messages, latest: Jul 22 2022 at 10:46)
• Automatic diagram chasing in double complex (1 message, latest: Jul 22 2022 at 07:29)
• substitution of prop in fol preserves validity (1 message, latest: Jul 21 2022 at 01:22)
• Rep k G is closed (25 messages, latest: Jul 20 2022 at 23:32)
• Definition of presheaf of modules (64 messages, latest: Jul 20 2022 at 05:13)
• Heights of posets (6 messages, latest: Jul 19 2022 at 22:25)
• Implementation of multiplicative characters (104 messages, latest: Jul 18 2022 at 18:36)
• Action G C diamond? (6 messages, latest: Jul 16 2022 at 18:37)
• supr is union of finite supr (25 messages, latest: Jul 16 2022 at 08:43)
• Selmer groups of number fields (10 messages, latest: Jul 16 2022 at 00:03)
• subobject_like class? (12 messages, latest: Jul 15 2022 at 11:48)
• pgame.short (2 messages, latest: Jul 14 2022 at 22:22)
• subalgebra.comap' (3 messages, latest: Jul 14 2022 at 14:18)
• Definition of circulant matrices (11 messages, latest: Jul 13 2022 at 22:13)
• Stirling (8 messages, latest: Jul 13 2022 at 19:47)
• diamond for rat.encodable (1 message, latest: Jul 12 2022 at 19:52)
• Game theory (15 messages, latest: Jul 12 2022 at 17:40)
• Localization preservers injective maps (22 messages, latest: Jul 09 2022 at 09:32)
• arithmetic timeout with a^2+b^2+c^2=7 (6 messages, latest: Jul 07 2022 at 19:26)
• ore localization (20 messages, latest: Jul 04 2022 at 19:38)
• Lagrange interpolants (171 messages, latest: Jul 04 2022 at 13:15)
• Gödel completeness theorem (16 messages, latest: Jul 04 2022 at 06:28)
• How to calculate derivatives (6 messages, latest: Jul 02 2022 at 10:16)
• universe levels in preserves statements (63 messages, latest: Jul 02 2022 at 06:55)
• ✔ Adding fin.induction_zero and induction_succ lemmas (1 message, latest: Jul 01 2022 at 17:18)
• Adding fin.induction_zero and induction_succ lemmas (5 messages, latest: Jun 29 2022 at 20:17)
• Separation axioms (2 messages, latest: Jun 29 2022 at 11:35)
• two different quotients by subgroup (25 messages, latest: Jun 29 2022 at 02:52)
• linear programming (9 messages, latest: Jun 28 2022 at 15:46)
• Definition of convex_cone (4 messages, latest: Jun 28 2022 at 02:24)
• normal closure (23 messages, latest: Jun 25 2022 at 06:15)
• ✔ Algebraic Conjugate in Finite Field (2 messages, latest: Jun 25 2022 at 01:04)
• Redefine metrizable_space etc (5 messages, latest: Jun 24 2022 at 19:13)
• ✔ Adjoint of linear map between hilbert spaces (2 messages, latest: Jun 23 2022 at 23:45)
• Adjoint of linear map between hilbert spaces (8 messages, latest: Jun 23 2022 at 23:02)
• Minkowski functional for nonreal scalars (19 messages, latest: Jun 22 2022 at 13:12)
• Scalar tower/restrict scalars for is_R_or_C (3 messages, latest: Jun 21 2022 at 18:28)
• Homotopy formalization (71 messages, latest: Jun 21 2022 at 04:22)
• Sesquilinear form notation (7 messages, latest: Jun 20 2022 at 23:20)
• change order on pfilter (5 messages, latest: Jun 20 2022 at 23:16)
• triggering is_scalar_tower (17 messages, latest: Jun 20 2022 at 20:33)
• Involution lattices and Heyting algebras (8 messages, latest: Jun 20 2022 at 10:50)
• Exterior algebras over semiring (47 messages, latest: Jun 18 2022 at 23:46)
• Undergraduate number theory student projects (44 messages, latest: Jun 18 2022 at 18:12)
• Quadratic Hilbert symbol over ℚ (376 messages, latest: Jun 16 2022 at 20:14)
• Redefining Sheaves (48 messages, latest: Jun 16 2022 at 13:41)
• is_open_pos_measure (8 messages, latest: Jun 16 2022 at 13:08)
• Left inverse to injection (13 messages, latest: Jun 16 2022 at 10:21)
• ✔ det_vandermonde_eq_zero (2 messages, latest: Jun 15 2022 at 19:16)
• Appearance of quot.sound in equiv_like.surjective (12 messages, latest: Jun 15 2022 at 15:43)
• det_vandermonde_eq_zero (19 messages, latest: Jun 15 2022 at 11:29)
• Feedback wanted on Hamming implmentation (10 messages, latest: Jun 14 2022 at 19:28)
• F.g. modules over PIDs (32 messages, latest: Jun 14 2022 at 13:58)
• Strange error in rewriting a cardinal term (9 messages, latest: Jun 13 2022 at 20:16)
• Basel problem / ζ(2) (17 messages, latest: Jun 13 2022 at 10:02)
• Construction of the Riemann Sphere (20 messages, latest: Jun 10 2022 at 09:49)
• Discrete metric. (29 messages, latest: Jun 09 2022 at 11:36)
• trouble setting up mathlib after upgrade (9 messages, latest: Jun 08 2022 at 09:28)
• Formalizing Gardam's disproof of a "Kaplansky Conjecture" (2 messages, latest: Jun 08 2022 at 01:12)
• epi_comp not an instance (5 messages, latest: Jun 07 2022 at 18:14)
• normalized_factors (10 messages, latest: Jun 07 2022 at 15:12)
• Question about Parametric Integrals (7 messages, latest: Jun 06 2022 at 17:38)
• Codisjointness (7 messages, latest: Jun 05 2022 at 20:34)
• Do we need complex.abs? (1 message, latest: Jun 02 2022 at 05:48)
• formula for ⊓ in subobject (15 messages, latest: Jun 02 2022 at 05:08)
• category theory rewrite in exactness tactic (13 messages, latest: Jun 01 2022 at 16:21)
• semi-mul_action_hom (28 messages, latest: Jun 01 2022 at 09:55)
• Dedekind-MacNeille completion. (17 messages, latest: Jun 01 2022 at 08:15)
• Intersecting families (4 messages, latest: May 31 2022 at 11:16)
• Seifert–van Kampen theorem (26 messages, latest: May 31 2022 at 06:23)
• Another theorem of Jordan (1 message, latest: May 30 2022 at 21:26)
• localization map for modules (87 messages, latest: May 30 2022 at 21:06)
• coordinate changes in a topological vector bundle (17 messages, latest: May 30 2022 at 14:36)
• metrizability (13 messages, latest: May 30 2022 at 14:05)
• complexes in the opposite category (2 messages, latest: May 30 2022 at 03:14)
• Infix notation for is_O/is_o (89 messages, latest: May 28 2022 at 05:04)
• pushout of biprod.fst and biprod.snd is zero (81 messages, latest: May 27 2022 at 12:57)
• Redefining Cantor's normal form (84 messages, latest: May 24 2022 at 19:07)
• bundles (11 messages, latest: May 24 2022 at 17:21)
• Division monoids and wheels (5 messages, latest: May 23 2022 at 17:20)
• Bornology (160 messages, latest: May 22 2022 at 23:15)
• contrapositive (6 messages, latest: May 19 2022 at 08:23)
• Web Editor math (14 messages, latest: May 18 2022 at 09:21)
• Simple lemma about irreducible polynomial factors (98 messages, latest: May 17 2022 at 16:38)
• How can we formulate Schanuel's conjecture in Lean? (3 messages, latest: May 15 2022 at 23:30)
• add_torsor order instances (57 messages, latest: May 15 2022 at 20:38)
• Convex hull of a product (19 messages, latest: May 15 2022 at 12:22)
• subobjects up to automorphisms? (2 messages, latest: May 15 2022 at 08:16)
• Do we need separated_space? (11 messages, latest: May 15 2022 at 08:02)
• topology on filters? (11 messages, latest: May 14 2022 at 16:08)
• help with a PR? (4 messages, latest: May 13 2022 at 10:59)
• Duplicate lemma (6 messages, latest: May 13 2022 at 07:50)
• Fermat's last theorem for n=3 (20 messages, latest: May 12 2022 at 14:53)
• Who came up with group filter bases? (4 messages, latest: May 11 2022 at 17:12)
• Preiss' theorem (2 messages, latest: May 11 2022 at 14:12)
• ✔ CI fails to catch elan (2 messages, latest: May 08 2022 at 11:04)
• CI fails to catch elan (2 messages, latest: May 08 2022 at 08:47)
• Laurent polynomials (22 messages, latest: May 07 2022 at 08:15)
• Linear combinations of \(t^ke^{λt}\) (9 messages, latest: May 07 2022 at 04:25)
• Sequential space (20 messages, latest: May 06 2022 at 14:40)
• "exp" in char p (13 messages, latest: May 06 2022 at 09:21)
• Is star_module sensible for non-commutative rings? (11 messages, latest: May 04 2022 at 10:54)
• Multiplicative subgroups of a ring (20 messages, latest: May 04 2022 at 02:06)
• matrix norms (14 messages, latest: May 02 2022 at 17:52)
• ✔ Proof of Cantor Injective? (1 message, latest: May 01 2022 at 17:56)
• Proof of Cantor Injective? (25 messages, latest: May 01 2022 at 16:55)
• "new" polynomial.coeff (346 messages, latest: Apr 28 2022 at 17:27)
• Computable real.sqrt (29 messages, latest: Apr 27 2022 at 22:45)
• maximum modulus principle (41 messages, latest: Apr 27 2022 at 02:18)
• Closure of a thickening (42 messages, latest: Apr 26 2022 at 09:58)
• Geometric sequence tends to 0 (7 messages, latest: Apr 25 2022 at 15:36)
• small sets filter (7 messages, latest: Apr 24 2022 at 22:20)
• Help with Normed Space Error (3 messages, latest: Apr 24 2022 at 16:58)
• Argument principle (21 messages, latest: Apr 22 2022 at 19:58)
• filter.comap (8 messages, latest: Apr 21 2022 at 22:26)
• Is the zero algebra normed? (87 messages, latest: Apr 21 2022 at 07:24)
• cardinality of powerset (41 messages, latest: Apr 20 2022 at 23:36)
• convolution of functions (38 messages, latest: Apr 20 2022 at 14:34)
• abelian categories (17 messages, latest: Apr 20 2022 at 10:49)
• Simple lemma with irreducible polynomial factors (2 messages, latest: Apr 17 2022 at 14:01)
• a small topology lemma (5 messages, latest: Apr 15 2022 at 18:48)
• family of linear maps is C^n if its applications are C^n (1 message, latest: Apr 15 2022 at 17:59)
• Some more about valuation rings (8 messages, latest: Apr 15 2022 at 06:50)
• Extraneous requirement in finprod.smul_finsum? (28 messages, latest: Apr 14 2022 at 23:12)
• Topological affine spaces (1 message, latest: Apr 14 2022 at 05:31)
• ✔ Stating continuity of coe_fn (4 messages, latest: Apr 11 2022 at 18:37)
• Stating continuity of coe_fn (1 message, latest: Apr 11 2022 at 18:16)
• Refactoring measure.map (11 messages, latest: Apr 09 2022 at 20:21)
• Proofs About Polynomial Degree Based on Derivative (47 messages, latest: Apr 09 2022 at 08:51)
• u sub in lean? (3 messages, latest: Apr 08 2022 at 23:53)
• working in namespace monoid (20 messages, latest: Apr 08 2022 at 15:32)
• frontier_closed_ball' (7 messages, latest: Apr 08 2022 at 14:17)
• Using partitions of unity (36 messages, latest: Apr 07 2022 at 19:49)
• Ax-Grothendieck (39 messages, latest: Apr 07 2022 at 15:51)
• The consistency of NF (Gabbay claimed proof) (3 messages, latest: Apr 07 2022 at 15:00)
• Naming mess (18 messages, latest: Apr 07 2022 at 09:09)
• pseudoelements (18 messages, latest: Apr 07 2022 at 06:43)
• fixing_subgroup etc. (3 messages, latest: Apr 06 2022 at 20:47)
• proof tactics suggestion (10 messages, latest: Apr 03 2022 at 11:11)
• Subsets (23 messages, latest: Apr 02 2022 at 00:08)
• super tactic (13 messages, latest: Apr 01 2022 at 22:34)
• approximate units (21 messages, latest: Mar 31 2022 at 19:29)
• N-ary image (4 messages, latest: Mar 29 2022 at 17:19)
• Notation for zero_at_infinity_continuous_map (15 messages, latest: Mar 28 2022 at 20:56)
• Type / Type* using cardinal (34 messages, latest: Mar 28 2022 at 20:32)
• dependent and (5 messages, latest: Mar 25 2022 at 11:20)
• Why does an ordered_semiring need to be add cancellative? (10 messages, latest: Mar 23 2022 at 06:02)
• polar coordinates (7 messages, latest: Mar 22 2022 at 15:43)
• induction on degree of polynomial (24 messages, latest: Mar 21 2022 at 11:56)
• [measurable_space α] [borel_space α] (4 messages, latest: Mar 20 2022 at 18:18)
• Group actions (37 messages, latest: Mar 19 2022 at 17:45)
• second degree equation (8 messages, latest: Mar 19 2022 at 16:36)
• analysis overview (4 messages, latest: Mar 17 2022 at 16:17)
• isocrystals (6 messages, latest: Mar 17 2022 at 15:53)
• Evaluation of continuous functions is continuous (20 messages, latest: Mar 17 2022 at 11:20)
• free groups (23 messages, latest: Mar 17 2022 at 08:51)
• Valuation rings (38 messages, latest: Mar 16 2022 at 15:27)
• target of ring hom algebra over image (38 messages, latest: Mar 16 2022 at 07:45)
• linear_combination for ≠ goals (16 messages, latest: Mar 14 2022 at 21:16)
• vector bundles – typeclass inference issue (27 messages, latest: Mar 14 2022 at 14:11)
• function doesn't reduce (10 messages, latest: Mar 14 2022 at 11:45)
• primitive actions (10 messages, latest: Mar 13 2022 at 22:56)
• model theory (62 messages, latest: Mar 13 2022 at 17:05)
• Extending add_monoid_hom and add_monoid_hom_class (29 messages, latest: Mar 13 2022 at 12:47)
• alternatives to tactic.omega (9 messages, latest: Mar 13 2022 at 01:13)
• balanced hull / seminorm split (14 messages, latest: Mar 12 2022 at 09:08)
• chain rule (2 messages, latest: Mar 12 2022 at 08:04)
• ✔ target of ring hom algebra over image (1 message, latest: Mar 12 2022 at 02:07)
• convergence of real-valued series (2 messages, latest: Mar 09 2022 at 07:56)
• ideal.mul_le_right (8 messages, latest: Mar 08 2022 at 22:53)
• classes: extends vs assumption (2 messages, latest: Mar 08 2022 at 22:40)
• ℤ\[√-2\] is a euclidean domain (18 messages, latest: Mar 08 2022 at 22:14)
• Ultraproducts (9 messages, latest: Mar 08 2022 at 16:38)
• polynomials from coefficient (14 messages, latest: Mar 08 2022 at 15:47)
• generalizing lemmas about monotone nat -> nat functions (12 messages, latest: Mar 08 2022 at 12:04)
• Un-classifying exact (1 message, latest: Mar 06 2022 at 09:45)
• norm_num with large numbers (29 messages, latest: Mar 05 2022 at 19:24)
• Defining cyclotomic polynomials (9 messages, latest: Mar 05 2022 at 15:42)
• ✔ norm_num and fin (2 messages, latest: Mar 05 2022 at 00:55)
• corprime and is_coprime (5 messages, latest: Mar 04 2022 at 19:20)
• norm_num and fin (12 messages, latest: Mar 04 2022 at 18:32)
• constructe proof (9 messages, latest: Mar 04 2022 at 13:30)
• Zeckendorf's theorem (37 messages, latest: Mar 04 2022 at 13:17)
• is_torsion Fq[X] (31 messages, latest: Mar 04 2022 at 01:00)
• Projective spaces (9 messages, latest: Mar 03 2022 at 22:50)
• bounding a \sum with a single element — where do I put this? (22 messages, latest: Mar 03 2022 at 18:23)
• ordinal.infinite (7 messages, latest: Mar 03 2022 at 15:07)
• generalising closed cartesian categories to closed monoidal (10 messages, latest: Mar 02 2022 at 01:46)
• Polar sets (2 messages, latest: Mar 01 2022 at 20:15)
• what is an injective object (75 messages, latest: Mar 01 2022 at 09:12)
• naming in operator algebras (6 messages, latest: Mar 01 2022 at 09:08)
• what is a derived functor (3 messages, latest: Feb 28 2022 at 20:57)
• Proving that group_filter_basis induces a group topology (8 messages, latest: Feb 27 2022 at 19:52)
• [C-algebras](topic/C-algebras.html) (93 messages, latest: Feb 27 2022 at 06:42)
• Normal elements of a star monoid: type class or not? (24 messages, latest: Feb 26 2022 at 09:01)
• Spectral theorem for bounded normal operators (4 messages, latest: Feb 25 2022 at 14:19)
• Valence formula (3 messages, latest: Feb 25 2022 at 09:16)
• Schur's lemma (95 messages, latest: Feb 25 2022 at 05:23)
• finsum in practice (24 messages, latest: Feb 25 2022 at 00:33)
• two vectors have the same direction (9 messages, latest: Feb 23 2022 at 13:18)
• orthonormal basis structure (70 messages, latest: Feb 22 2022 at 23:31)
• times_cont_diff name (14 messages, latest: Feb 22 2022 at 21:09)
• Ping pong lemma! (1 message, latest: Feb 22 2022 at 13:43)
• representations of sl2 (12 messages, latest: Feb 22 2022 at 11:06)
• (partial) spanish translation of formalizing mathematics (5 messages, latest: Feb 21 2022 at 13:56)
• Complex analysis (14 messages, latest: Feb 21 2022 at 02:36)
• tendsto mixing nat and int (19 messages, latest: Feb 19 2022 at 15:58)
• Classes in Model Theory (9 messages, latest: Feb 19 2022 at 04:22)
• induced topology commutes with product (17 messages, latest: Feb 18 2022 at 15:09)
• sum grouping adjacent terms (7 messages, latest: Feb 16 2022 at 19:03)
• p power of tsum le of tsum of p powers (4 messages, latest: Feb 15 2022 at 15:41)
• quotient vs orbits (7 messages, latest: Feb 14 2022 at 21:01)
• type of pair term (3 messages, latest: Feb 13 2022 at 19:13)
• Computing Roth numbers (122 messages, latest: Feb 12 2022 at 23:45)
• Should fields be Dedekind domains? (13 messages, latest: Feb 11 2022 at 09:10)
• FLT for n=3 (9 messages, latest: Feb 11 2022 at 07:57)
• ✔ direct product of sylow groups (39 messages, latest: Feb 10 2022 at 10:17)
• compactly supported functions (8 messages, latest: Feb 08 2022 at 18:25)
• Engel's theorem? (52 messages, latest: Feb 08 2022 at 13:36)
• HoTT on wellformedness of contexts (10 messages, latest: Feb 08 2022 at 10:13)
• Modal algebra (7 messages, latest: Feb 08 2022 at 10:09)
• union of complete sets (20 messages, latest: Feb 08 2022 at 07:20)
• Krull topology on Galois groups (47 messages, latest: Feb 07 2022 at 20:30)
• gelfand formula (13 messages, latest: Feb 07 2022 at 10:57)
• equality of lambda-abstractions in HoTT (21 messages, latest: Feb 06 2022 at 15:51)
• metric_space (fin n) (15 messages, latest: Feb 05 2022 at 16:08)
• infinite products of commutators (8 messages, latest: Feb 05 2022 at 12:35)
• ✔ Function of empty codomain (5 messages, latest: Feb 05 2022 at 08:51)
• Bicompactness (8 messages, latest: Feb 05 2022 at 08:05)
• Function of empty codomain (8 messages, latest: Feb 05 2022 at 07:59)
• Strange type error with fintype_sdiff (37 messages, latest: Feb 05 2022 at 03:54)
• ✔ Fubini for infinite series (1 message, latest: Feb 04 2022 at 16:21)
• Ord (4 messages, latest: Feb 04 2022 at 11:39)
• 1-limits in Cat (26 messages, latest: Feb 03 2022 at 23:47)
• commutator of products (12 messages, latest: Feb 03 2022 at 20:50)
• interval integral: do we need α ≠ real? (18 messages, latest: Feb 03 2022 at 12:12)
• box integrals: ι or fin n (6 messages, latest: Feb 03 2022 at 04:18)
• Why is is_limit data? (5 messages, latest: Feb 02 2022 at 18:56)
• Fubini for infinite series (5 messages, latest: Feb 02 2022 at 13:29)
• Integrals in other systems? (36 messages, latest: Feb 02 2022 at 10:03)
• the power basis of a conjugate (26 messages, latest: Feb 01 2022 at 14:35)
• failed to unify (15 messages, latest: Jan 31 2022 at 10:58)
• HoTT (222 messages, latest: Jan 31 2022 at 09:38)
• Heyting algebra (7 messages, latest: Jan 30 2022 at 18:07)
• direct product of sylow groups (24 messages, latest: Jan 30 2022 at 11:53)
• congr_arg (7 messages, latest: Jan 29 2022 at 03:48)
• Eiseinstein polynomials (26 messages, latest: Jan 26 2022 at 16:11)
• ✔ fintype (sylow p G) (1 message, latest: Jan 26 2022 at 14:31)
• Name for certain map in Hilbert spaces (43 messages, latest: Jan 26 2022 at 09:03)
• fintype (sylow p G) (5 messages, latest: Jan 25 2022 at 21:44)
• Proj construction (55 messages, latest: Jan 25 2022 at 12:42)
• Finitely supported product (4 messages, latest: Jan 24 2022 at 20:59)
• Do we need has_norm (30 messages, latest: Jan 24 2022 at 15:08)
• ✔ normal sylow groups (2 messages, latest: Jan 24 2022 at 13:38)
• monoid_hom.map (14 messages, latest: Jan 24 2022 at 13:01)
• normal sylow groups (16 messages, latest: Jan 23 2022 at 19:12)
• Universe restriction for sheaves (18 messages, latest: Jan 21 2022 at 18:14)
• ✔ nilpotency → normalizer_condition (2 messages, latest: Jan 21 2022 at 18:12)
• nilpotency → normalizer_condition (5 messages, latest: Jan 21 2022 at 15:59)
• ✔ nilpotency questions (1 message, latest: Jan 21 2022 at 15:55)
• nilpotency questions (9 messages, latest: Jan 21 2022 at 14:07)
• ongoing measure_theory refactor (7 messages, latest: Jan 18 2022 at 11:34)
• ✔ Weakening docs#submodule.mul_induction_on (1 message, latest: Jan 18 2022 at 10:40)
• |-x| (12 messages, latest: Jan 18 2022 at 08:55)
• How "normal" is ring_nf normal form? (4 messages, latest: Jan 18 2022 at 01:06)
• Weakening docs#submodule.mul_induction_on (13 messages, latest: Jan 17 2022 at 23:02)
• solvable groups (11 messages, latest: Jan 17 2022 at 13:09)
• unitary submonoid (9 messages, latest: Jan 17 2022 at 11:33)
• ✔ Antilinear functions over the reals (1 message, latest: Jan 15 2022 at 23:35)
• Antilinear functions over the reals (6 messages, latest: Jan 15 2022 at 20:55)
• Locally convex spaces (51 messages, latest: Jan 15 2022 at 10:10)
• Toward Jordan Normal Form (8 messages, latest: Jan 14 2022 at 19:00)
• null_of_locally_null (5 messages, latest: Jan 14 2022 at 16:30)
• Timeouts with Ext (18 messages, latest: Jan 14 2022 at 01:01)
• monoid and smul for seminorms (7 messages, latest: Jan 13 2022 at 00:45)
• getting started proving filter.ne_bot (20 messages, latest: Jan 12 2022 at 19:31)
• equivalence between bounded integers and nat (8 messages, latest: Jan 11 2022 at 10:33)
• induction on fin n (19 messages, latest: Jan 11 2022 at 00:10)
• Order on partitions (24 messages, latest: Jan 10 2022 at 12:45)
• slope and dslope (3 messages, latest: Jan 09 2022 at 21:43)
• Symplectic geometry (15 messages, latest: Jan 09 2022 at 11:49)
• Fourier series (2 messages, latest: Jan 09 2022 at 09:38)
• C^r smoothness with non-integer r (14 messages, latest: Jan 09 2022 at 08:51)
• comap of ultrafilter of surjective function (29 messages, latest: Jan 08 2022 at 22:59)
• ✔ How to get the unique term is a type of "cardinal 1" (2 messages, latest: Jan 07 2022 at 17:17)
• ✔ Parsing nim definition (14 messages, latest: Jan 07 2022 at 00:40)
• How to get the unique term is a type of "cardinal 1" (17 messages, latest: Jan 07 2022 at 00:11)
• notation for algebra_map (45 messages, latest: Jan 06 2022 at 15:38)
• Non-unital rings (9 messages, latest: Jan 05 2022 at 18:26)
• ✔ PR : signature from cycle type (4 messages, latest: Jan 04 2022 at 12:06)
• Modular forms and related things (67 messages, latest: Jan 04 2022 at 09:07)
• category of topological groups (46 messages, latest: Jan 03 2022 at 09:54)
• Modulus of convexity (3 messages, latest: Jan 02 2022 at 21:30)
• defining the category ConvGroup (9 messages, latest: Jan 02 2022 at 16:26)
• order and topology (6 messages, latest: Jan 01 2022 at 20:37)
• is_foo v foo (12 messages, latest: Dec 31 2021 at 22:10)
• ✔ technical debts (4 messages, latest: Dec 30 2021 at 21:23)
• Lp space (13 messages, latest: Dec 29 2021 at 22:26)
• Ultrafilters on Boolean Algebras (27 messages, latest: Dec 29 2021 at 18:19)
• ✔ fintype of subset (6 messages, latest: Dec 28 2021 at 18:48)
• The alternating group is simple! (32 messages, latest: Dec 28 2021 at 15:53)
• Symmetrized product of a real algebra (23 messages, latest: Dec 28 2021 at 11:19)
• Cauchy integral formula (36 messages, latest: Dec 27 2021 at 23:17)
• map_prod (4 messages, latest: Dec 27 2021 at 22:04)
• thoughts on topologies on automorphism groups (7 messages, latest: Dec 27 2021 at 17:25)
• Missing theorems (49 messages, latest: Dec 27 2021 at 13:10)
• Lemma location (5 messages, latest: Dec 27 2021 at 11:54)
• Lifting an equivalence to sym2 (17 messages, latest: Dec 26 2021 at 11:42)
• generates/measurable (4 messages, latest: Dec 25 2021 at 15:51)
• Cyclotomic fields (212 messages, latest: Dec 25 2021 at 05:35)
• semiorthogonal decompositions (12 messages, latest: Dec 24 2021 at 09:51)
• Lie bracket on endomorphisms of addative commutative group (27 messages, latest: Dec 24 2021 at 08:49)
• Metrisability of compact-open topology (110 messages, latest: Dec 23 2021 at 20:49)
• Semi(bi)linear maps with invertible ring_hom (23 messages, latest: Dec 23 2021 at 12:32)
• powers of x<1 (4 messages, latest: Dec 23 2021 at 09:44)
• Traversable functor for finset (3 messages, latest: Dec 22 2021 at 23:28)
• defining partial group actions (48 messages, latest: Dec 21 2021 at 17:10)
• Rings as instances of non-unital, non-associative rings (6 messages, latest: Dec 21 2021 at 08:42)
• ICM talk (202 messages, latest: Dec 20 2021 at 14:21)
• Monadic structure of finsupp (18 messages, latest: Dec 20 2021 at 12:07)
• ✔ extracting forall from iff (6 messages, latest: Dec 18 2021 at 00:01)
• Finite product of finite modules is finite (25 messages, latest: Dec 17 2021 at 18:45)
• mul_assoc is backwards (12 messages, latest: Dec 16 2021 at 09:49)
• Combinatorial Nullstellensatz (8 messages, latest: Dec 15 2021 at 23:06)
• ✔ Convergence at border points (4 messages, latest: Dec 14 2021 at 22:04)
• Convergence at border points (24 messages, latest: Dec 14 2021 at 20:19)
• continuous group actions (22 messages, latest: Dec 14 2021 at 18:21)
• filter convergence and tendsto (16 messages, latest: Dec 14 2021 at 16:30)
• Notation for nhds_within (23 messages, latest: Dec 14 2021 at 08:56)
• definition of sheaf of modules (28 messages, latest: Dec 11 2021 at 17:05)
• functions in full subcategories (7 messages, latest: Dec 10 2021 at 04:54)
• manifolds without corners (26 messages, latest: Dec 09 2021 at 12:16)
• complex.has_scalar (32 messages, latest: Dec 08 2021 at 11:46)
• Chain lemmas (4 messages, latest: Dec 07 2021 at 17:51)
• Why formalize mathematics (43 messages, latest: Dec 07 2021 at 09:18)
• not integrable (10 messages, latest: Dec 07 2021 at 09:14)
• ideal.quotient (20 messages, latest: Dec 06 2021 at 21:18)
• additive ramsey theory (5 messages, latest: Dec 06 2021 at 21:18)
• subsets of fintypes (21 messages, latest: Dec 06 2021 at 21:13)
• Nothing uses directed_system.map_self (3 messages, latest: Dec 06 2021 at 13:31)
• circle integral (4 messages, latest: Dec 06 2021 at 06:20)
• alg_hom (5 messages, latest: Dec 05 2021 at 23:00)
• ✔ membership in finset.sum (1 message, latest: Dec 04 2021 at 10:57)
• ✔ summable vs has_sum (2 messages, latest: Dec 04 2021 at 10:56)
• membership in finset.sum (12 messages, latest: Dec 03 2021 at 22:16)
• summable vs has_sum (7 messages, latest: Dec 03 2021 at 21:07)
• Zonotopes (1 message, latest: Dec 03 2021 at 16:11)
• pre-inner product spaces (18 messages, latest: Dec 03 2021 at 01:03)
• filter subtype lift (6 messages, latest: Nov 30 2021 at 13:09)
• nonempty spectrum (32 messages, latest: Nov 30 2021 at 02:09)
• mul_actions (14 messages, latest: Nov 29 2021 at 20:42)
• is_singleton Prop? (8 messages, latest: Nov 29 2021 at 18:28)
• filter.has_antitone_basis (6 messages, latest: Nov 25 2021 at 21:19)
• Notation for group(module,ideal) quotients (26 messages, latest: Nov 25 2021 at 19:13)
• Determinant bound (11 messages, latest: Nov 25 2021 at 17:55)
• nat.coprime vs is_coprime (27 messages, latest: Nov 25 2021 at 08:07)
• ✔ setoid.ker, kinda (5 messages, latest: Nov 22 2021 at 18:40)
• setoid.ker, kinda (8 messages, latest: Nov 22 2021 at 18:09)
• Should ideal.map take a plain function (1 message, latest: Nov 22 2021 at 15:38)
• abstract polytopes (14 messages, latest: Nov 22 2021 at 02:32)
• interval_integrable (12 messages, latest: Nov 21 2021 at 17:44)
• Bounded bilinear forms (80 messages, latest: Nov 20 2021 at 16:05)
• ✔ lint test optimization (31 messages, latest: Nov 17 2021 at 15:14)
• orthogonal group generated by reflections (8 messages, latest: Nov 16 2021 at 19:20)
• ord.connected allows empty sets (14 messages, latest: Nov 15 2021 at 20:44)
• Power basis of L=K(x) (4 messages, latest: Nov 15 2021 at 17:41)
• Facts on sheaves and schemes via constructive logic (13 messages, latest: Nov 14 2021 at 14:41)
• ae_measurable vs null_measurable (14 messages, latest: Nov 11 2021 at 12:31)
• is_scalar_tower for polynomial rings (4 messages, latest: Nov 10 2021 at 15:37)
• universe restriction on limit (20 messages, latest: Nov 10 2021 at 11:22)
• convergence of a power series (26 messages, latest: Nov 09 2021 at 21:33)
• product measures (61 messages, latest: Nov 09 2021 at 13:06)
• quotient groups (36 messages, latest: Nov 08 2021 at 23:31)
• zmod n to ℚ (7 messages, latest: Nov 08 2021 at 22:25)
• Add opposite (43 messages, latest: Nov 08 2021 at 17:52)
• graph theory (497 messages, latest: Nov 08 2021 at 15:20)
• Strict convexity of the norm (3 messages, latest: Nov 07 2021 at 15:12)
• canonical group_with_zero {-1,0,1} (31 messages, latest: Nov 06 2021 at 09:48)
• lint test optimization (5 messages, latest: Nov 05 2021 at 13:16)
• Guidance Help (4 messages, latest: Nov 05 2021 at 00:04)
• Tietze extension theorem (5 messages, latest: Nov 04 2021 at 01:21)
• Limits and colimits of quivers and categories (12 messages, latest: Nov 03 2021 at 22:23)
• seminormed group (44 messages, latest: Nov 02 2021 at 18:17)
• subalgebra.under (7 messages, latest: Nov 02 2021 at 12:43)
• comm_semiring axioms (6 messages, latest: Oct 30 2021 at 13:42)
• Trying to define maximal subgroups (17 messages, latest: Oct 29 2021 at 13:23)
• smul invariant measure (6 messages, latest: Oct 29 2021 at 07:24)
• measurable embedding (16 messages, latest: Oct 28 2021 at 23:56)
• how to avoid int_algebra diamond (86 messages, latest: Oct 28 2021 at 20:47)
• Associahedron (70 messages, latest: Oct 28 2021 at 13:56)
• global variables (4 messages, latest: Oct 27 2021 at 18:03)
• Small addition to topology.connected (24 messages, latest: Oct 27 2021 at 13:51)
• Determinant of adjugate matrix (20 messages, latest: Oct 27 2021 at 10:33)
• memory issue (26 messages, latest: Oct 26 2021 at 13:06)
• Picard-Lindelof (5 messages, latest: Oct 26 2021 at 06:58)
• ring.inverse (13 messages, latest: Oct 26 2021 at 06:54)
• ✔ collaboration question (4 messages, latest: Oct 25 2021 at 22:09)
• complexity theory (3 messages, latest: Oct 25 2021 at 22:08)
• collaboration question (4 messages, latest: Oct 25 2021 at 21:03)
• Gluing topological spaces (45 messages, latest: Oct 24 2021 at 18:56)
• an optimization problem (17 messages, latest: Oct 23 2021 at 12:25)
• Style question: iff, or both directions and iff (8 messages, latest: Oct 22 2021 at 20:42)
• Splitting analysis.special_functions.exp_log (7 messages, latest: Oct 22 2021 at 14:29)
• Redefine rpow? (14 messages, latest: Oct 22 2021 at 13:37)
• norm_pos_iff' etc (5 messages, latest: Oct 22 2021 at 07:25)
• The Hodge Conjecture (7 messages, latest: Oct 22 2021 at 04:27)
• continuous_linear_map.arrow_congr (4 messages, latest: Oct 19 2021 at 23:51)
• product of (pre)connected spaces (15 messages, latest: Oct 17 2021 at 17:39)
• nat.cast_sub (4 messages, latest: Oct 17 2021 at 14:42)
• Incorrect number of universe levels parameters (11 messages, latest: Oct 16 2021 at 06:52)
• Equalities of morphisms (6 messages, latest: Oct 15 2021 at 21:42)
• Question about induction(s) (30 messages, latest: Oct 15 2021 at 17:46)
• Convex space (160 messages, latest: Oct 15 2021 at 00:12)
• Zero rank modules (2 messages, latest: Oct 14 2021 at 16:01)
• Topology of finite-dimensional real vector spaces (17 messages, latest: Oct 14 2021 at 07:45)
• Geodesic spaces (7 messages, latest: Oct 13 2021 at 16:49)
• Liouville numbers (7 messages, latest: Oct 13 2021 at 16:45)
• ✔ Universes maze (7 messages, latest: Oct 13 2021 at 08:49)
• Definition of normed_algebra (65 messages, latest: Oct 12 2021 at 11:20)
• Simplicial complex (66 messages, latest: Oct 11 2021 at 10:39)
• complex conj vs has_star.star (48 messages, latest: Oct 10 2021 at 00:04)
• Universes and sheaves (6 messages, latest: Oct 08 2021 at 22:44)
• Infinite index definition (31 messages, latest: Oct 06 2021 at 21:10)
• Barycentric coordinates (15 messages, latest: Oct 05 2021 at 22:47)
• Issues with manifolds (21 messages, latest: Oct 05 2021 at 20:31)
• summable_geometric_of_norm_lt_1 works for ℝ yet fails for ℂ (11 messages, latest: Oct 04 2021 at 20:49)
• Q-algebra diamond (43 messages, latest: Oct 04 2021 at 13:06)
• dinatural transformations (330 messages, latest: Oct 03 2021 at 11:29)
• strict convexity (19 messages, latest: Oct 02 2021 at 14:06)
• ✔ mysterious hang bug (40 messages, latest: Oct 01 2021 at 20:25)
• mysterious hang bug (7 messages, latest: Oct 01 2021 at 20:11)
• project: nth-roots in alg closed fields (8 messages, latest: Oct 01 2021 at 18:46)
• Strong rank condition for commutative rings (41 messages, latest: Oct 01 2021 at 15:15)
• homotopy - naming collision (32 messages, latest: Sep 30 2021 at 12:28)
• circular predicate (4 messages, latest: Sep 30 2021 at 05:31)
• Contribute a project on Hadamard matrices (73 messages, latest: Sep 28 2021 at 12:39)
• complex order (12 messages, latest: Sep 28 2021 at 11:23)
• eventually monotone (48 messages, latest: Sep 27 2021 at 20:43)
• New folder analysis/inner_product_space (5 messages, latest: Sep 25 2021 at 14:37)
• simp-normal form in set_theory.cardinal (4 messages, latest: Sep 25 2021 at 07:33)
• categorical subobjects (3 messages, latest: Sep 24 2021 at 15:32)
• measure_equiv (2 messages, latest: Sep 22 2021 at 12:39)
• Overuse of algebra type class (7 messages, latest: Sep 22 2021 at 12:32)
• zmod algebra diamond (3 messages, latest: Sep 20 2021 at 08:30)
• Laplace transform (1 message, latest: Sep 19 2021 at 17:20)
• Group action refactor (31 messages, latest: Sep 19 2021 at 17:07)
• universal algebra and filtered colimits (10 messages, latest: Sep 18 2021 at 10:29)
• polynomial.ring_hom_ext (25 messages, latest: Sep 18 2021 at 06:46)
• linear_map.to_matrix_alg_equiv (3 messages, latest: Sep 17 2021 at 20:56)
• Z_p is a Henselian local ring (31 messages, latest: Sep 17 2021 at 12:50)
• char_poly vs charpoly (3 messages, latest: Sep 16 2021 at 14:32)
• preserve filtered colimits (107 messages, latest: Sep 15 2021 at 15:46)
• diagram chasing in abelian categories (16 messages, latest: Sep 14 2021 at 14:46)
• mv_polynomial.vars (16 messages, latest: Sep 13 2021 at 08:53)
• subfields (66 messages, latest: Sep 13 2021 at 08:24)
• TC normal form (6 messages, latest: Sep 12 2021 at 18:45)
• Caratheodory (137 messages, latest: Sep 11 2021 at 18:02)
• Expository source on Peano axioms for undergrads? (56 messages, latest: Sep 11 2021 at 10:52)
• to_additive and smul of measures (10 messages, latest: Sep 11 2021 at 07:52)
• subalgebra pain (21 messages, latest: Sep 10 2021 at 15:41)
• antimono (20 messages, latest: Sep 09 2021 at 21:12)
• Lost instance (23 messages, latest: Sep 09 2021 at 16:21)
• Transporting along is_scalar_tower (30 messages, latest: Sep 09 2021 at 09:06)
• Definition of convex_on (21 messages, latest: Sep 06 2021 at 15:42)
• W-hyperbolic spaces (4 messages, latest: Sep 06 2021 at 11:50)
• ordered_comm_monoid (17 messages, latest: Sep 06 2021 at 07:28)
• lists (50 messages, latest: Sep 03 2021 at 02:42)
• rigid (autonomous) categories (43 messages, latest: Sep 01 2021 at 17:42)
• ✔ rewriting under a binder (8 messages, latest: Sep 01 2021 at 13:57)
• equivalence relations = partitions (6 messages, latest: Aug 30 2021 at 20:19)
• Alternative proofs (12 messages, latest: Aug 30 2021 at 15:54)
• basis.tensor_product (9 messages, latest: Aug 30 2021 at 11:00)
• Relaxing from UFDs to Euclidean domains (8 messages, latest: Aug 30 2021 at 09:08)
• reindex_apply (12 messages, latest: Aug 26 2021 at 17:49)
• Where should these lemmas go? (12 messages, latest: Aug 25 2021 at 12:10)
• nonlinear PDE? (11 messages, latest: Aug 22 2021 at 15:02)
• Algebras generated by a submodule (2 messages, latest: Aug 20 2021 at 20:36)
• Ostrowski theorems formalized in Lean 3 (43 messages, latest: Aug 20 2021 at 15:02)
• decreasing induction (6 messages, latest: Aug 20 2021 at 00:39)
• set.finite.fintype (42 messages, latest: Aug 16 2021 at 14:59)
• winning position (8 messages, latest: Aug 16 2021 at 11:07)
• Using mem_carrier ? (17 messages, latest: Aug 16 2021 at 07:27)
• domain vs domain (7 messages, latest: Aug 11 2021 at 16:52)
• reassociate to prune goals? (4 messages, latest: Aug 06 2021 at 15:13)
• Cyclically ordered group (2 messages, latest: Aug 04 2021 at 21:42)
• definition of is_nilpotent (8 messages, latest: Aug 04 2021 at 11:05)
• Alternative proofs of Liouville's theorem on conformal maps (3 messages, latest: Aug 03 2021 at 09:58)
• Stars and bars (5 messages, latest: Jul 31 2021 at 08:01)
• field extensions and linear independence (11 messages, latest: Jul 30 2021 at 11:43)
• Identifying equal (?) sets (10 messages, latest: Jul 29 2021 at 17:18)
• McCune's axiom (166 messages, latest: Jul 24 2021 at 19:42)
• Determinant for low rank (41 messages, latest: Jul 20 2021 at 20:23)
• Formalizing conformal maps (41 messages, latest: Jul 19 2021 at 19:34)
• Inf on ordinal (5 messages, latest: Jul 18 2021 at 06:51)
• Challenge with homology (14 messages, latest: Jul 18 2021 at 06:45)
• What's new in Lean maths? (400 messages, latest: Jul 16 2021 at 21:32)
• Partition of unity (26 messages, latest: Jul 15 2021 at 15:55)
• quiz (5 messages, latest: Jul 12 2021 at 07:47)
• equiconsistent to ZFC (10 messages, latest: Jul 12 2021 at 02:45)
• Conformal maps (10 messages, latest: Jul 08 2021 at 14:24)
• signed measure (26 messages, latest: Jul 06 2021 at 13:37)
• groupoids (6 messages, latest: Jul 06 2021 at 08:10)
• ordered_module on nat and int (24 messages, latest: Jul 02 2021 at 15:27)
• busywork (41 messages, latest: Jul 02 2021 at 11:21)
• Kumar Eswaran's proof of RH (5 messages, latest: Jul 01 2021 at 10:54)
• the future of subring (29 messages, latest: Jun 30 2021 at 13:56)
• naming (18 messages, latest: Jun 30 2021 at 13:09)
• Refactoring localization_map (40 messages, latest: Jun 30 2021 at 09:16)
• Simple functions in Lp (9 messages, latest: Jun 29 2021 at 06:08)
• is_dedekind_domain_dvr_equiv_is_dedekind_domain_inv (11 messages, latest: Jun 28 2021 at 13:50)
• Cardinality of a finset (10 messages, latest: Jun 28 2021 at 10:48)
• Simplicial API (13 messages, latest: Jun 27 2021 at 16:03)
• Abstraction in Equation (6 messages, latest: Jun 26 2021 at 10:25)
• local diffeomorphism (2 messages, latest: Jun 23 2021 at 20:45)
• mul_action_hom.map_matrix (21 messages, latest: Jun 23 2021 at 20:03)
• cardinality of insert (24 messages, latest: Jun 23 2021 at 16:23)
• some newbie questions about following progress (16 messages, latest: Jun 22 2021 at 17:48)
• Abelian Subgroup (17 messages, latest: Jun 21 2021 at 21:49)
• simplex category (13 messages, latest: Jun 21 2021 at 16:07)
• 2 <= 3 log 2 (5 messages, latest: Jun 20 2021 at 13:11)
• invalid structure header (3 messages, latest: Jun 16 2021 at 18:02)
• add_monoid_hom and ordered_embedding (9 messages, latest: Jun 15 2021 at 17:15)
• finite free modules (181 messages, latest: Jun 15 2021 at 15:44)
• basis.sum_extend (15 messages, latest: Jun 15 2021 at 08:48)
• countable De Bruijn–Erdős theorem (46 messages, latest: Jun 14 2021 at 19:34)
• Determinant of an element of orthogonal/unitary groups (1 message, latest: Jun 14 2021 at 17:44)
• linear_map.ker_eq_bot semiring? (5 messages, latest: Jun 13 2021 at 04:09)
• projective space (42 messages, latest: Jun 11 2021 at 19:18)
• quotient_ring_saturate (3 messages, latest: Jun 11 2021 at 13:10)
• filter.mem_map (13 messages, latest: Jun 10 2021 at 16:09)
• Pi instances (3 messages, latest: Jun 09 2021 at 12:10)
• rearranging indices in a summable (12 messages, latest: Jun 07 2021 at 11:23)
• is_projective (6 messages, latest: Jun 07 2021 at 10:52)
• hatcher cell complex (15 messages, latest: Jun 06 2021 at 06:05)
• add_monoid_hom.comp_assoc is the wrong way around (34 messages, latest: Jun 05 2021 at 21:36)
• coe_add vs add_coe (10 messages, latest: Jun 04 2021 at 10:28)
• Summing Laurent Series (5 messages, latest: May 31 2021 at 19:50)
• linearly independent sets are smaller than bases? (19 messages, latest: May 31 2021 at 11:46)
• nat.sqrt and pow 2 (2 messages, latest: May 28 2021 at 21:21)
• list of missing lemmas, theorems (5 messages, latest: May 27 2021 at 01:19)
• adjoint example (44 messages, latest: May 24 2021 at 03:44)
• LMFDB natively in Lean (5 messages, latest: May 23 2021 at 21:46)
• Bounded supremum on conditionally_complete_lattice (13 messages, latest: May 23 2021 at 16:37)
• 0! (9 messages, latest: May 23 2021 at 05:11)
• algebra order refactor (16 messages, latest: May 22 2021 at 09:55)
• Characteristics of fraction_ring (6 messages, latest: May 20 2021 at 11:00)
• Invariant basis number: finite version implies infinite? (22 messages, latest: May 20 2021 at 09:17)
• Cyclotomic polynomials (192 messages, latest: May 18 2021 at 13:30)
• explicit polynomials (3 messages, latest: May 16 2021 at 17:09)
• modeq_mul_cancel_left (6 messages, latest: May 16 2021 at 14:39)
• closed of discrete (12 messages, latest: May 15 2021 at 18:50)
• (⨁ i, Mᵢ i) →+ M parsing (2 messages, latest: May 15 2021 at 18:07)
• Infinite cyclic permutations (16 messages, latest: May 14 2021 at 19:04)
• Conjugation Action (34 messages, latest: May 13 2021 at 23:12)
• char_zero (111 messages, latest: May 13 2021 at 20:05)
• function.injective.add_comm_group (4 messages, latest: May 13 2021 at 20:04)
• gal of cyclotomic polynomial (11 messages, latest: May 13 2021 at 08:53)
• subspace (1 message, latest: May 13 2021 at 06:01)
• regular measure (3 messages, latest: May 12 2021 at 16:33)
• ring_hom (14 messages, latest: May 11 2021 at 11:21)
• Define multiplication on games (surreal numbers) (9 messages, latest: May 10 2021 at 18:16)
• Naming conventions for theorems about quotients (4 messages, latest: May 09 2021 at 12:25)
• Should these go into mathlib? (13 messages, latest: May 07 2021 at 17:11)
• cycle notation (7 messages, latest: May 07 2021 at 15:43)
• alternative definition of naturals (41 messages, latest: May 07 2021 at 01:14)
• Duplication is_integral R x / x ∈ integral_closure R x (25 messages, latest: May 07 2021 at 00:50)
• Instance for (quotient pgame.setoid) (15 messages, latest: May 06 2021 at 15:57)
• concrete_category.coe_{id,comp} (5 messages, latest: May 06 2021 at 08:05)
• discrete quotients and partitions (31 messages, latest: May 04 2021 at 20:22)
• Binomial theorem (26 messages, latest: May 02 2021 at 20:01)
• derived functors (5 messages, latest: Apr 29 2021 at 13:43)
• Removing duplicates from an open cover (74 messages, latest: Apr 29 2021 at 12:05)
• ordered stuff (104 messages, latest: Apr 28 2021 at 14:02)
• content of finsupp (16 messages, latest: Apr 28 2021 at 12:56)
• grading by submonoids maths question (48 messages, latest: Apr 27 2021 at 23:09)
• Millenium Problems (56 messages, latest: Apr 27 2021 at 20:19)
• ring tactic for types (44 messages, latest: Apr 27 2021 at 17:27)
• Hahn Series (31 messages, latest: Apr 24 2021 at 22:31)
• Small and large categories in Type Theory (65 messages, latest: Apr 21 2021 at 08:39)
• has_deriv_at.continuous_on (25 messages, latest: Apr 21 2021 at 08:22)
• Schemes in Isabelle/HOL (94 messages, latest: Apr 20 2021 at 20:29)
• trivial group (12 messages, latest: Apr 20 2021 at 17:16)
• projective objects (16 messages, latest: Apr 20 2021 at 07:49)
• Definition of primitive (4 messages, latest: Apr 20 2021 at 06:34)
• intrinsic interior/frontier/closure (1 message, latest: Apr 19 2021 at 15:21)
• linear_isometry_complex (185 messages, latest: Apr 19 2021 at 07:36)
• [linear_ordered_noncommgroup(_with_zero)](topic/linear_orderednoncomm_group(_with_zero).html) (21 messages, latest: Apr 19 2021 at 07:03)
• recursive definitions (17 messages, latest: Apr 14 2021 at 18:18)
• Gradings on a ring (59 messages, latest: Apr 14 2021 at 14:44)
• Unique differentiability and definitional equality (4 messages, latest: Apr 12 2021 at 20:01)
• Pseudo-lattice? (4 messages, latest: Apr 09 2021 at 17:58)
• vector space (65 messages, latest: Apr 09 2021 at 15:03)
• interval_integrable.comp (23 messages, latest: Apr 09 2021 at 05:28)
• Sups of ℕ and infinity (17 messages, latest: Apr 08 2021 at 15:19)
• multilinear_map: f (c • x) = c ^ fintype.card ι • f x (14 messages, latest: Apr 08 2021 at 15:14)
• ordered rings (4 messages, latest: Apr 06 2021 at 06:07)
• functoriality of lists and zip_with (10 messages, latest: Apr 05 2021 at 22:55)
• maximal independent family (127 messages, latest: Apr 05 2021 at 11:56)
• GL(n) (17 messages, latest: Apr 01 2021 at 13:01)
• Sheaf condition for type-valued sheaf (28 messages, latest: Mar 31 2021 at 12:11)
• linarith power (12 messages, latest: Mar 31 2021 at 10:09)
• Conjugacy Classes (5 messages, latest: Mar 26 2021 at 17:21)
• fastest approach to proving equation iffs (19 messages, latest: Mar 26 2021 at 13:18)
• inner_product_space ℝ (euclidean_space 𝕜 n)? (28 messages, latest: Mar 26 2021 at 01:29)
• 2-categories (26 messages, latest: Mar 25 2021 at 22:01)
• Unifying fin (n+2) and fin (n+1) (29 messages, latest: Mar 24 2021 at 21:45)
• Equate Intersections (5 messages, latest: Mar 24 2021 at 19:19)
• non-natural exponents? (17 messages, latest: Mar 24 2021 at 11:47)
• Naming contest: FreeMat? (31 messages, latest: Mar 24 2021 at 07:12)
• copies of matrices (18 messages, latest: Mar 23 2021 at 23:00)
• Towards Whitney's embedding theorem (4 messages, latest: Mar 23 2021 at 19:39)
• has_continuous_smul (4 messages, latest: Mar 23 2021 at 13:58)
• \[comm_ring R\] vs \[ring R\] \[comm R\] (34 messages, latest: Mar 23 2021 at 12:35)
• Covers (7 messages, latest: Mar 23 2021 at 08:22)
• Index of intersection (20 messages, latest: Mar 22 2021 at 23:44)
• category of groups (8 messages, latest: Mar 22 2021 at 21:27)
• "new" complexes (9 messages, latest: Mar 22 2021 at 11:03)
• long exact sequences (60 messages, latest: Mar 22 2021 at 01:11)
• Topos theory so far (6 messages, latest: Mar 19 2021 at 17:23)
• Difficulty of formalizing Hartshorne's exercises (6 messages, latest: Mar 19 2021 at 14:28)
• finite free over PID (10 messages, latest: Mar 17 2021 at 09:23)
• Simplicial sets (18 messages, latest: Mar 16 2021 at 17:27)
• Faulhaber's Theorem (sum of kth powers) (62 messages, latest: Mar 16 2021 at 07:14)
• A general theory of isomorphism (1 message, latest: Mar 14 2021 at 22:20)
• subgroup of free group is free (20 messages, latest: Mar 13 2021 at 22:24)
• additive discrete valuation (64 messages, latest: Mar 13 2021 at 17:29)
• to_additive mismatch (31 messages, latest: Mar 12 2021 at 17:12)
• eq_zero_of_norm_lt (6 messages, latest: Mar 12 2021 at 08:42)
• Name? (32 messages, latest: Mar 12 2021 at 06:46)
• live lecture on H^0 and H^1 (1 message, latest: Mar 11 2021 at 15:02)
• metric space stuff (2 messages, latest: Mar 11 2021 at 12:34)
• distrib – I take it all back (22 messages, latest: Mar 11 2021 at 07:37)
• conj_mul_eq_abs_sq_left (3 messages, latest: Mar 11 2021 at 00:53)
• notation for nnnorm (17 messages, latest: Mar 10 2021 at 20:03)
• trivialization of fiber bundles over intervals (14 messages, latest: Mar 09 2021 at 20:58)
• Subset of structure (6 messages, latest: Mar 09 2021 at 20:37)
• Magma algebras (38 messages, latest: Mar 08 2021 at 17:15)
• abel multiplication (13 messages, latest: Mar 07 2021 at 21:28)
• manifold atlas (4 messages, latest: Mar 07 2021 at 08:44)
• group theory: lagrange theorem (7 messages, latest: Mar 06 2021 at 03:50)
• Use instances with local hypothesis (7 messages, latest: Mar 05 2021 at 19:40)
• What are the arrows in R ⟶ S induces S-Alg ⥤ R-Alg (15 messages, latest: Mar 05 2021 at 16:35)
• how obvious is "obvious" (20 messages, latest: Mar 05 2021 at 12:00)
• nonarchimedean rings (15 messages, latest: Mar 05 2021 at 04:25)
• Conjugate-linear (103 messages, latest: Mar 04 2021 at 18:21)
• affine independence help (2 messages, latest: Mar 04 2021 at 00:31)
• Highest universe level encountered in practice (32 messages, latest: Mar 02 2021 at 08:46)
• paracompact spaces (4 messages, latest: Mar 02 2021 at 00:28)
• Gaussian integral (6 messages, latest: Mar 02 2021 at 00:22)
• fincard and cardinal.to_nat (13 messages, latest: Mar 01 2021 at 20:09)
• class group of a number field (45 messages, latest: Mar 01 2021 at 13:30)
• Trees (2 messages, latest: Feb 28 2021 at 09:16)
• finite presentation of element of a tensor product (21 messages, latest: Feb 26 2021 at 12:45)
• Type expected error (11 messages, latest: Feb 26 2021 at 12:42)
• Internal Direct Sum (34 messages, latest: Feb 25 2021 at 09:56)
• truth and provability (33 messages, latest: Feb 24 2021 at 04:05)
• Additive functors (60 messages, latest: Feb 22 2021 at 23:23)
• Slow instance (83 messages, latest: Feb 22 2021 at 18:23)
• is_scalar_tower for morprhisms (20 messages, latest: Feb 21 2021 at 05:43)
• monomial diamond? (11 messages, latest: Feb 21 2021 at 03:16)
• decidable problem (4 messages, latest: Feb 19 2021 at 10:16)
• universe issue (27 messages, latest: Feb 18 2021 at 23:16)
• deep recursion error for squeeze_simp (4 messages, latest: Feb 18 2021 at 17:32)
• ∀ᶠ (x : α) in F, P x and ∃ᶠ (39 messages, latest: Feb 18 2021 at 12:07)
• order on prime_spectrum (61 messages, latest: Feb 17 2021 at 23:21)
• to_finset_inter (29 messages, latest: Feb 16 2021 at 19:08)
• smul_eq_mul (37 messages, latest: Feb 16 2021 at 14:41)
• well-defined function (3 messages, latest: Feb 14 2021 at 12:12)
• totally_disconnected uses subsingleton, not set.subsingleton (3 messages, latest: Feb 14 2021 at 07:34)
• Different linear orders on reals (6 messages, latest: Feb 13 2021 at 20:24)
• complete_lattice (with_top ℕ) (15 messages, latest: Feb 12 2021 at 17:56)
• why are manifolds difficult? (37 messages, latest: Feb 10 2021 at 07:34)
• new monoid struture on nat (49 messages, latest: Feb 08 2021 at 18:56)
• isomorphism of rings of integers with different radices (10 messages, latest: Feb 08 2021 at 06:03)
• Non-positive-definite inner product spaces (10 messages, latest: Feb 04 2021 at 14:57)
• "formal concepts" + SVD (6 messages, latest: Jan 30 2021 at 16:40)
• (comm_)semiring: examples? (207 messages, latest: Jan 29 2021 at 21:19)
• Abel-Ruffini theorem announced in Coq (12 messages, latest: Jan 22 2021 at 19:35)
• Homeless lemma (54 messages, latest: Jan 20 2021 at 11:13)
• Transferring equiv.perm over embeddings (18 messages, latest: Jan 14 2021 at 10:51)
• FTC-2 on open set (17 messages, latest: Jan 14 2021 at 04:55)
• has_sum_nat_add_iff for add_monoid? (104 messages, latest: Jan 12 2021 at 20:41)
• Orthogonal/Unitary Group (25 messages, latest: Jan 11 2021 at 22:36)
• Fubini's for fin 2 -> R (5 messages, latest: Jan 11 2021 at 03:29)
• finset from "finsubtype" (7 messages, latest: Jan 10 2021 at 03:02)
• sigma_finite measures (9 messages, latest: Jan 08 2021 at 23:41)
• Order reversing iso (31 messages, latest: Jan 08 2021 at 19:33)
• log (6 messages, latest: Jan 08 2021 at 14:10)
• Definition of nat multiplication (13 messages, latest: Jan 08 2021 at 12:50)
• Modular Lattice (10 messages, latest: Jan 07 2021 at 18:40)
• One integral away from Euler's summation formula (25 messages, latest: Jan 07 2021 at 12:11)
• Stokes theorem (4 messages, latest: Jan 06 2021 at 00:09)
• Radical in Noetherian Ring (6 messages, latest: Jan 05 2021 at 21:46)
• maths in Lean 4 standard library (1 message, latest: Jan 05 2021 at 21:02)
• Icc_ssubset_Icc (54 messages, latest: Jan 05 2021 at 09:12)
• Dedekind domains (107 messages, latest: Jan 04 2021 at 17:58)
• Linear independence in torsion modules (25 messages, latest: Jan 03 2021 at 00:13)
• algebra problem (25 messages, latest: Jan 01 2021 at 22:11)
• Semisimple modules (17 messages, latest: Dec 31 2020 at 19:12)
• Subobject correspondences (10 messages, latest: Dec 31 2020 at 08:41)
• Explicit hypothesis vs implication hypothesis convention (10 messages, latest: Dec 29 2020 at 08:35)
• roption.dom vs multiplicity.finite (2 messages, latest: Dec 28 2020 at 12:10)
• Limit of polynomials (47 messages, latest: Dec 27 2020 at 06:11)
• Adjacent Transpositions (6 messages, latest: Dec 25 2020 at 08:27)
• rfl lemma (8 messages, latest: Dec 23 2020 at 22:53)
• witt vectors (388 messages, latest: Dec 23 2020 at 09:52)
• Bimodules (74 messages, latest: Dec 23 2020 at 00:12)
• Instances for is_R_or_C (19 messages, latest: Dec 21 2020 at 05:35)
• Why small diagrams? (13 messages, latest: Dec 20 2020 at 19:23)
• Atoms in order and algebra (8 messages, latest: Dec 20 2020 at 19:09)
• There are no canonically_linear_ordered_monoids (10 messages, latest: Dec 17 2020 at 18:07)
• Orthogonal projection (17 messages, latest: Dec 17 2020 at 14:30)
• Étale morphisms of rings (139 messages, latest: Dec 17 2020 at 13:58)
• opt_param (4 messages, latest: Dec 17 2020 at 09:27)
• computations in double sum (11 messages, latest: Dec 14 2020 at 09:39)
• matrix.congr (7 messages, latest: Dec 11 2020 at 14:49)
• direct sum vs dfinsupp (3 messages, latest: Dec 10 2020 at 18:29)
• eq_to_hom in category theory (20 messages, latest: Dec 10 2020 at 09:51)
• Lists: head versus last (48 messages, latest: Dec 08 2020 at 17:32)
• Working with subtypes. (19 messages, latest: Dec 07 2020 at 23:36)
• Error when applying supr_le (32 messages, latest: Dec 07 2020 at 22:15)
• What is this operator? (27 messages, latest: Dec 07 2020 at 14:35)
• Translation/rotation number for various maps (16 messages, latest: Dec 07 2020 at 14:21)
• Inductive type of elements defined by radicals (14 messages, latest: Dec 05 2020 at 05:32)
• Limits in a category (49 messages, latest: Dec 04 2020 at 14:26)
• tsum (4 messages, latest: Dec 04 2020 at 04:47)
• Group Algebras? (7 messages, latest: Dec 04 2020 at 01:34)
• Exterior Algebra (55 messages, latest: Dec 03 2020 at 18:04)
• Submonoids containing the base/central ring (47 messages, latest: Dec 03 2020 at 17:17)
• type class instance error (11 messages, latest: Dec 02 2020 at 17:29)
• Differential Rings (41 messages, latest: Dec 02 2020 at 02:43)
• monoid structure on set G (2 messages, latest: Nov 29 2020 at 01:03)
• Minimal polynomial over ℚ vs over ℤ (28 messages, latest: Nov 28 2020 at 16:52)
• (anti)-monotone (104 messages, latest: Nov 28 2020 at 02:23)
• Galois theory (17 messages, latest: Nov 27 2020 at 17:53)
• Moebius inversion (6 messages, latest: Nov 25 2020 at 18:22)
• dealing with multiple instanciation (31 messages, latest: Nov 25 2020 at 13:54)
• Improve ring_theory/localization (1 message, latest: Nov 24 2020 at 16:38)
• epsilon delta limit definitions (4 messages, latest: Nov 24 2020 at 07:41)
• Induction on subsets of a finset (27 messages, latest: Nov 22 2020 at 23:47)
• mv_polynomial induction on variables (24 messages, latest: Nov 22 2020 at 05:38)
• Friday afternoon puzzle – 37 ∈ 37? (85 messages, latest: Nov 21 2020 at 19:52)
• Using linarith with my own class (36 messages, latest: Nov 21 2020 at 01:19)
• Two universe levels (34 messages, latest: Nov 20 2020 at 16:27)
• sheaves on a site (4 messages, latest: Nov 18 2020 at 14:29)
• Free stuff (240 messages, latest: Nov 18 2020 at 09:24)
• How to formalize recursion theorem? (65 messages, latest: Nov 18 2020 at 00:41)
• getting a ring from an integral domain (68 messages, latest: Nov 13 2020 at 19:25)
• field iff all ideals are trivial (5 messages, latest: Nov 13 2020 at 09:04)
• measurable derivative/integral (45 messages, latest: Nov 11 2020 at 22:16)
• measure on R^n (5 messages, latest: Nov 07 2020 at 23:40)
• Constructing an algebra equiv in term mode (14 messages, latest: Nov 07 2020 at 12:48)
• Defining has_inv when only some elements have an inverse (21 messages, latest: Nov 06 2020 at 19:11)
• has_deriv_at.?comp naming (8 messages, latest: Nov 06 2020 at 16:00)
• Isomorphism of Field Extensions (100 messages, latest: Nov 02 2020 at 23:20)
• Timeout (10 messages, latest: Nov 02 2020 at 14:35)
• Constructing a complete lattice (23 messages, latest: Nov 01 2020 at 02:41)
• integer multiplication and nlinarith (22 messages, latest: Oct 31 2020 at 05:19)
• tensor algebras and a construction (19 messages, latest: Oct 30 2020 at 18:07)
• deterministic timeout (5 messages, latest: Oct 29 2020 at 18:13)
• Exponential form of a complex number (43 messages, latest: Oct 28 2020 at 23:17)
• use? (21 messages, latest: Oct 27 2020 at 09:47)
• condensed mathematics (235 messages, latest: Oct 26 2020 at 19:34)
• Constructing Polynomials (12 messages, latest: Oct 25 2020 at 23:50)
• Restriction of a groupoid (9 messages, latest: Oct 22 2020 at 18:52)
• coe_fn (9 messages, latest: Oct 21 2020 at 21:24)
• restrict scalars of linear map (12 messages, latest: Oct 21 2020 at 14:39)
• Simplicial homotopy theory (2 messages, latest: Oct 20 2020 at 23:01)
• max resolution depth reached (15 messages, latest: Oct 20 2020 at 15:11)
• Definition of polynomial.splits (14 messages, latest: Oct 20 2020 at 07:01)
• decidable linear order (31 messages, latest: Oct 20 2020 at 03:48)
• Bundling direction into affine_subspace (5 messages, latest: Oct 19 2020 at 19:23)
• How to explicitly give an implicit argument (14 messages, latest: Oct 19 2020 at 19:18)
• The sigma algebra generated by a family of measurable fcts (18 messages, latest: Oct 19 2020 at 17:30)
• Notation for affine_map (20 messages, latest: Oct 19 2020 at 17:16)
• The Type of R-algebras (27 messages, latest: Oct 19 2020 at 13:54)
• char_zero and char_p (4 messages, latest: Oct 19 2020 at 07:48)
• law of excluded middle in set membership (62 messages, latest: Oct 18 2020 at 23:41)
• Showing topological_space_eq "manually" (11 messages, latest: Oct 18 2020 at 20:47)
• Can a constructor in an inductive family take in an index (55 messages, latest: Oct 18 2020 at 14:07)
• Defining a function on an inductive type (17 messages, latest: Oct 18 2020 at 12:35)
• Teaching functions (20 messages, latest: Oct 17 2020 at 20:24)
• Showing equality of finite sets (31 messages, latest: Oct 17 2020 at 18:37)
• How is readability valued in the mathlib (8 messages, latest: Oct 17 2020 at 17:18)
• multilple "and elimination" (9 messages, latest: Oct 17 2020 at 17:15)
• Is there a Hölder inequality in the Matthlib? (7 messages, latest: Oct 16 2020 at 21:32)
• polynomial functions (24 messages, latest: Oct 16 2020 at 16:08)
• Issue using nat.cast_max (26 messages, latest: Oct 16 2020 at 16:05)
• tensor product of modules (17 messages, latest: Oct 16 2020 at 15:34)
• Can't find algebra instance (9 messages, latest: Oct 16 2020 at 15:09)
• nat.cast_coe (11 messages, latest: Oct 16 2020 at 03:46)
• Adjunctions (4 messages, latest: Oct 15 2020 at 13:27)
• polynomial.map (4 messages, latest: Oct 15 2020 at 11:43)
• Bell and Tsirelson inequalities (16 messages, latest: Oct 14 2020 at 16:39)
• (Ho)TT question on showing functions equal in identity type (4 messages, latest: Oct 14 2020 at 10:11)
• Lean job in London (1 message, latest: Oct 13 2020 at 22:38)
• Naming for monoid_algebra k G (51 messages, latest: Oct 12 2020 at 13:55)
• naming: lie_smul (16 messages, latest: Oct 12 2020 at 06:04)
• Compact Hausdorff spaces (3 messages, latest: Oct 10 2020 at 00:22)
• Right implementation of Hilbert Plane? (4 messages, latest: Oct 09 2020 at 23:31)
• ultrafilter.Lim (2 messages, latest: Oct 09 2020 at 15:08)
• kleisli vs kleisli (8 messages, latest: Oct 09 2020 at 00:09)
• linear_ordered_semiring (8 messages, latest: Oct 08 2020 at 13:39)
• reversing the coefficients (151 messages, latest: Oct 06 2020 at 13:00)
• odd numbers (10 messages, latest: Oct 06 2020 at 09:25)
• Conjugate-linear maps (15 messages, latest: Oct 05 2020 at 16:03)
• euclidean names (34 messages, latest: Oct 05 2020 at 11:29)
• times_cont_diff_at (5 messages, latest: Oct 05 2020 at 05:34)
• Radon-Nikodym Theorem (28 messages, latest: Oct 04 2020 at 19:32)
• Simplifying 0 < a * b etc (32 messages, latest: Oct 02 2020 at 23:10)
• to_additive, gpow, smul (14 messages, latest: Oct 01 2020 at 20:07)
• I still don't understand how to use extends (6 messages, latest: Sep 30 2020 at 21:26)
• Reasonable theorem to formalize (1 message, latest: Sep 30 2020 at 20:49)
• OEIS Lean entries (43 messages, latest: Sep 30 2020 at 00:26)
• Grading the tensor_algebra (71 messages, latest: Sep 29 2020 at 16:51)
• algebra is not scaling for me (298 messages, latest: Sep 29 2020 at 07:41)
• Lemma naming contest (17 messages, latest: Sep 28 2020 at 21:17)
• measurability of special functions (11 messages, latest: Sep 28 2020 at 19:29)
• help with mfderiv (21 messages, latest: Sep 28 2020 at 01:13)
• cheap IMO problem (18 messages, latest: Sep 27 2020 at 15:51)
• Minimal polynomials (16 messages, latest: Sep 26 2020 at 10:44)
• reorganising category_theory/limits/limits.lean (4 messages, latest: Sep 26 2020 at 01:29)
• interval arithmetic and Lean (12 messages, latest: Sep 25 2020 at 18:22)
• 2 * pi * I (7 messages, latest: Sep 25 2020 at 17:31)
• range of cos (10 messages, latest: Sep 25 2020 at 12:43)
• mv_power_series (4 messages, latest: Sep 25 2020 at 03:54)
• Ultrafilter map continuous (24 messages, latest: Sep 24 2020 at 23:31)
• Interval integral module docstring (11 messages, latest: Sep 24 2020 at 21:11)
• convex polytopes (26 messages, latest: Sep 24 2020 at 19:06)
• de Moivre (6 messages, latest: Sep 24 2020 at 18:52)
• Dangerous instance vs elaboration problems (17 messages, latest: Sep 22 2020 at 13:22)
• finite_dimensional assumption (8 messages, latest: Sep 21 2020 at 23:57)
• dot universe notation (7 messages, latest: Sep 21 2020 at 13:51)
• infinite sums / reals (20 messages, latest: Sep 21 2020 at 13:50)
• get_limit_cone (6 messages, latest: Sep 21 2020 at 13:34)
• polynomial.funext (7 messages, latest: Sep 21 2020 at 11:14)
• Arithmetic Functions (54 messages, latest: Sep 20 2020 at 06:14)
• Fermat's Last Theorem for n=4 (32 messages, latest: Sep 17 2020 at 20:01)
• subgroup module docstring. (10 messages, latest: Sep 15 2020 at 06:39)
• Refactoring UFDs to Monoids (129 messages, latest: Sep 15 2020 at 01:51)
• has_mem instance for factor_set (10 messages, latest: Sep 14 2020 at 16:21)
• Qbar (11 messages, latest: Sep 14 2020 at 14:00)
• schemes over k (11 messages, latest: Sep 14 2020 at 09:42)
• limits in functor categories (16 messages, latest: Sep 11 2020 at 03:06)
• injectivity of localization map (11 messages, latest: Sep 10 2020 at 13:33)
• How does Godel manifest in Type theory? (11 messages, latest: Sep 09 2020 at 06:25)
• Hermitian and semidefinite matrices (6 messages, latest: Sep 08 2020 at 23:41)
• why lean for math? (5 messages, latest: Sep 08 2020 at 15:07)
• Quadratic fields (15 messages, latest: Sep 05 2020 at 16:06)
• rw (14 messages, latest: Sep 03 2020 at 16:53)
• adjoining multiple elements notation (45 messages, latest: Sep 02 2020 at 23:46)
• Support in order ideal (11 messages, latest: Sep 02 2020 at 06:31)
• dead integral code (4 messages, latest: Sep 02 2020 at 06:12)
• polynomial ring homs (5 messages, latest: Sep 02 2020 at 03:38)
• Maps between zmod (16 messages, latest: Sep 01 2020 at 22:09)
• #4013 properties of ring homomorphisms (20 messages, latest: Sep 01 2020 at 14:28)
• equivalent definitions (9 messages, latest: Sep 01 2020 at 09:11)
• alternate definitions (30 messages, latest: Sep 01 2020 at 08:53)
• prop_limits branch (34 messages, latest: Sep 01 2020 at 08:03)
• Subring inclusion (3 messages, latest: Sep 01 2020 at 03:28)
• is_interval (48 messages, latest: Aug 31 2020 at 22:56)
• embeddings and hook arrow notation: (regular) monomorphisms (5 messages, latest: Aug 31 2020 at 22:56)
• o-minimality repo (58 messages, latest: Aug 31 2020 at 11:28)
• Errors with order hierarchy (18 messages, latest: Aug 31 2020 at 04:33)
• Inherit field instance from carrier (27 messages, latest: Aug 29 2020 at 19:18)
• Lie groups and Lie algebras (46 messages, latest: Aug 28 2020 at 20:11)
• Card structure on Group (31 messages, latest: Aug 28 2020 at 18:27)
• invalid type ascription (3 messages, latest: Aug 28 2020 at 17:34)
• limit notation (5 messages, latest: Aug 26 2020 at 06:28)
• local properties on charted spaces (11 messages, latest: Aug 25 2020 at 14:03)
• f-adic ring (47 messages, latest: Aug 23 2020 at 07:52)
• Definition of affine.simplex (8 messages, latest: Aug 22 2020 at 18:37)
• convexity (19 messages, latest: Aug 22 2020 at 15:05)
• Matroids - How to define? (57 messages, latest: Aug 22 2020 at 02:45)
• Localization of categories (50 messages, latest: Aug 22 2020 at 01:47)
• Lean can't figure out type of {a} (50 messages, latest: Aug 21 2020 at 21:19)
• Basic lemmas/instances about subfields (19 messages, latest: Aug 21 2020 at 16:09)
• naming contest (3 messages, latest: Aug 21 2020 at 08:50)
• ACC/DCC (7 messages, latest: Aug 21 2020 at 04:49)
• making PR about transcendental numbers (10 messages, latest: Aug 20 2020 at 17:34)
• limits and choice (90 messages, latest: Aug 20 2020 at 02:45)
• Little lemma about subfields (46 messages, latest: Aug 19 2020 at 16:03)
• module.restrict_scalars (16 messages, latest: Aug 18 2020 at 09:13)
• Real Closed Fields (18 messages, latest: Aug 18 2020 at 01:02)
• model completeness of algebraically closed fields (37 messages, latest: Aug 17 2020 at 16:57)
• Intuitionistic maths (20 messages, latest: Aug 17 2020 at 16:39)
• linear suffering (35 messages, latest: Aug 17 2020 at 14:54)
• Racks and Quandles (16 messages, latest: Aug 17 2020 at 14:04)
• boundary of a manifold (31 messages, latest: Aug 17 2020 at 07:34)
• order_iso (36 messages, latest: Aug 17 2020 at 06:03)
• Kan extensions of functors (2 messages, latest: Aug 17 2020 at 05:59)
• Construction of Algebraic Closure (82 messages, latest: Aug 17 2020 at 02:28)
• FTC-2 (12 messages, latest: Aug 15 2020 at 21:08)
• aa = bc -> gcd a b > 1 (14 messages, latest: Aug 15 2020 at 19:52)
• aa = bc -> gcd a b = min a b (4 messages, latest: Aug 15 2020 at 14:03)
• Snake Lemma (3 messages, latest: Aug 14 2020 at 12:24)
• non-trivial kernel iff determinant zero (6 messages, latest: Aug 14 2020 at 05:50)
• non-trivial kernel implies determinant zero (5 messages, latest: Aug 14 2020 at 00:58)
• Cantor's diagonal theorem (4 messages, latest: Aug 13 2020 at 04:39)
• Union_of_directed (6 messages, latest: Aug 12 2020 at 20:49)
• topos (84 messages, latest: Aug 12 2020 at 00:15)
• Schemes (6 messages, latest: Aug 11 2020 at 19:48)
• Banach-Tarski Paradox (3 messages, latest: Aug 11 2020 at 15:07)
• Polynomial composition and map commute (10 messages, latest: Aug 11 2020 at 03:45)
• universe hell in linear algebra (76 messages, latest: Aug 11 2020 at 00:36)
• Hi I'm int2, here's my recursor (60 messages, latest: Aug 10 2020 at 22:08)
• Using a basis of size one (4 messages, latest: Aug 09 2020 at 06:17)
• Formalizing the ternary Goldbach conjecture (17 messages, latest: Aug 07 2020 at 11:50)
• with_zero (multiplicative int) (16 messages, latest: Aug 06 2020 at 19:50)
• Pointed monoid (49 messages, latest: Aug 06 2020 at 13:02)
• Category structure on nat (32 messages, latest: Aug 06 2020 at 00:09)
• subrings (147 messages, latest: Aug 04 2020 at 22:14)
• from preorder to category (7 messages, latest: Aug 04 2020 at 15:24)
• composing a list of functions (105 messages, latest: Aug 04 2020 at 14:57)
• Definition of strict_mono (6 messages, latest: Aug 03 2020 at 03:27)
• golfing Ico union (104 messages, latest: Aug 03 2020 at 00:08)
• simplicial sets (1 message, latest: Aug 02 2020 at 11:15)
• sheaves on a base, etc. (20 messages, latest: Jul 31 2020 at 17:45)
• FTC progress report (4 messages, latest: Jul 31 2020 at 11:45)
• division ring to nontrivial semiring (11 messages, latest: Jul 30 2020 at 08:32)
• monoid objects again (95 messages, latest: Jul 30 2020 at 07:26)
• Bijective Ring Homorphism an Isomorphism (7 messages, latest: Jul 30 2020 at 03:55)
• nhds_left and nhds_right (18 messages, latest: Jul 29 2020 at 20:29)
• Notation for filter.principal (7 messages, latest: Jul 29 2020 at 14:45)
• I don't understand forall in flypitch (14 messages, latest: Jul 29 2020 at 07:54)
• Linear embeddings (18 messages, latest: Jul 28 2020 at 19:45)
• eventually_eq and sets (13 messages, latest: Jul 28 2020 at 16:37)
• fintype issues (27 messages, latest: Jul 28 2020 at 09:37)
• filter on sets (4 messages, latest: Jul 27 2020 at 20:32)
• trivial group / module (6 messages, latest: Jul 26 2020 at 03:12)
• sheaves of modules (39 messages, latest: Jul 25 2020 at 14:12)
• Understanding the definition of nhds (15 messages, latest: Jul 25 2020 at 11:22)
• Reusing monoid, group, etc over equivalences (41 messages, latest: Jul 25 2020 at 03:51)
• Haar measures (3 messages, latest: Jul 24 2020 at 22:10)
• gpowers (10 messages, latest: Jul 24 2020 at 21:10)
• add_group to group (4 messages, latest: Jul 24 2020 at 19:54)
• normalizers (5 messages, latest: Jul 24 2020 at 12:11)
• dfinsupp of product is dfinsupp of dfinsupp (14 messages, latest: Jul 24 2020 at 07:42)
• Fintype as measurable spaces? (20 messages, latest: Jul 23 2020 at 21:32)
• Derivations (16 messages, latest: Jul 23 2020 at 21:15)
• Morphisms in concrete categories (7 messages, latest: Jul 22 2020 at 14:42)
• locally ringed spaces (29 messages, latest: Jul 22 2020 at 09:27)
• subring (4 messages, latest: Jul 22 2020 at 05:57)
• notation for mv_polynomial.aeval (19 messages, latest: Jul 21 2020 at 16:03)
• prod vs prod_mk (20 messages, latest: Jul 20 2020 at 10:18)
• Norm of 1 (39 messages, latest: Jul 19 2020 at 13:23)
• Extensionality of homs (16 messages, latest: Jul 18 2020 at 21:58)
• algebraically closed fields (10 messages, latest: Jul 18 2020 at 17:48)
• has_continuous_mul (3 messages, latest: Jul 18 2020 at 15:46)
• integral of positive measurable functions (6 messages, latest: Jul 18 2020 at 14:36)
• from "exists" to sets (13 messages, latest: Jul 16 2020 at 17:58)
• ideal v vector space (30 messages, latest: Jul 16 2020 at 12:08)
• polynomial refactor (73 messages, latest: Jul 16 2020 at 05:43)
• trash can (1 message, latest: Jul 16 2020 at 03:32)
• definition of module (9 messages, latest: Jul 15 2020 at 13:23)
• Second-to-Leading Coefficient (25 messages, latest: Jul 15 2020 at 00:40)
• make an explicit group (7 messages, latest: Jul 14 2020 at 22:15)
• has_emptyc (13 messages, latest: Jul 14 2020 at 22:01)
• simp-ing of preimages (6 messages, latest: Jul 14 2020 at 21:01)
• too big for ring (32 messages, latest: Jul 14 2020 at 13:31)
• completion of module wrt ideal (29 messages, latest: Jul 14 2020 at 06:55)
• Class instance problem (11 messages, latest: Jul 13 2020 at 18:41)
• The Myhill-Nerode theorem, proved using regular expressions (8 messages, latest: Jul 12 2020 at 14:05)
• integral refactor (24 messages, latest: Jul 12 2020 at 01:53)
• transcendence of \(e\) (8 messages, latest: Jul 12 2020 at 00:17)
• coercion from ℚ to ℝ (30 messages, latest: Jul 11 2020 at 09:42)
• X^k - X ≠ 0 (8 messages, latest: Jul 10 2020 at 21:14)
• deriv (7 messages, latest: Jul 10 2020 at 16:05)
• Tensor product of matrices (19 messages, latest: Jul 10 2020 at 01:24)
• Restriction in structure groupoid (10 messages, latest: Jul 09 2020 at 20:37)
• Universe issue (11 messages, latest: Jul 09 2020 at 18:32)
• lift from subring to field (13 messages, latest: Jul 09 2020 at 14:12)
• multilinear right curry (27 messages, latest: Jul 08 2020 at 12:59)
• open subset of the reals (27 messages, latest: Jul 08 2020 at 05:15)
• submodule.span or ideal.span? (4 messages, latest: Jul 07 2020 at 14:12)
• more questions about where to put lemmas (1 message, latest: Jul 07 2020 at 13:36)
• normal subgroup : group :: ?? : semimodule (18 messages, latest: Jul 06 2020 at 18:35)
• Lean for the curious mathematician (210 messages, latest: Jul 06 2020 at 15:28)
• with_top \Z (17 messages, latest: Jul 06 2020 at 15:17)
• Instance confusion (8 messages, latest: Jul 06 2020 at 14:27)
• nonsingleton (107 messages, latest: Jul 06 2020 at 13:04)
• Product manifolds (15 messages, latest: Jul 04 2020 at 15:25)
• Alternative representations of Z (27 messages, latest: Jul 03 2020 at 19:27)
• defeq of reals (13 messages, latest: Jul 03 2020 at 10:17)
• Typeclass hierarchy graph (2 messages, latest: Jul 02 2020 at 20:17)
• omega.nat.le_and_le_iff_eq (2 messages, latest: Jul 02 2020 at 14:22)
• span_singleton_eq_bot simp? (10 messages, latest: Jul 02 2020 at 13:08)
• Naming request (5 messages, latest: Jul 01 2020 at 18:48)
• ZFC in Lean (26 messages, latest: Jul 01 2020 at 09:25)
• Perfect Numbers (93 messages, latest: Jul 01 2020 at 04:21)
• tactic or term mode proof? (45 messages, latest: Jun 30 2020 at 14:55)
• Cayley-Hamilton (249 messages, latest: Jun 30 2020 at 10:16)
• Multiplication on int is well-defined (21 messages, latest: Jun 29 2020 at 13:50)
• symmetric polynomials (13 messages, latest: Jun 29 2020 at 06:51)
• category theory tutorial maintenance (8 messages, latest: Jun 28 2020 at 20:00)
• int is a ring (5 messages, latest: Jun 28 2020 at 15:48)
• zero ring (80 messages, latest: Jun 28 2020 at 12:17)
• pythagorean triples (3 messages, latest: Jun 28 2020 at 00:09)
• rational numbers (4 messages, latest: Jun 27 2020 at 22:36)
• auto-generating names for declarations (24 messages, latest: Jun 27 2020 at 16:57)
• about polynomial.nat_degree (3 messages, latest: Jun 26 2020 at 08:54)
• Picking sides (37 messages, latest: Jun 25 2020 at 19:45)
• local ring refactor (25 messages, latest: Jun 25 2020 at 14:39)
• where should these definitions live? (6 messages, latest: Jun 25 2020 at 09:36)
• playing with nlinarith (16 messages, latest: Jun 24 2020 at 07:45)
• trivial submodules (6 messages, latest: Jun 24 2020 at 06:16)
• is_integral_of_finite_extension (7 messages, latest: Jun 23 2020 at 23:39)
• extends has_scalar (9 messages, latest: Jun 23 2020 at 21:59)
• topology predicate names (16 messages, latest: Jun 23 2020 at 18:23)
• integrals (8 messages, latest: Jun 22 2020 at 20:16)
• Inversion is analytic (21 messages, latest: Jun 22 2020 at 19:09)
• norm_cast failure (3 messages, latest: Jun 21 2020 at 16:06)
• Ideal (9 messages, latest: Jun 21 2020 at 12:19)
• tensor products of algebras (27 messages, latest: Jun 20 2020 at 10:38)
• Haar Measure (13 messages, latest: Jun 19 2020 at 07:30)
• Uniform Space Twitch stream (4 messages, latest: Jun 18 2020 at 14:08)
• uniform_continuous_on (6 messages, latest: Jun 17 2020 at 14:58)
• Extending an abbreviated structure (19 messages, latest: Jun 17 2020 at 02:57)
• Manifold constructors (3 messages, latest: Jun 16 2020 at 11:07)
• does CCC preserve category equivalence (33 messages, latest: Jun 16 2020 at 04:35)
• lie groups (39 messages, latest: Jun 15 2020 at 10:35)
• Complex inner product (133 messages, latest: Jun 15 2020 at 03:52)
• "projects" (3 messages, latest: Jun 14 2020 at 19:26)
• VSCode not showing errors (8 messages, latest: Jun 13 2020 at 15:19)
• bundling (35 messages, latest: Jun 13 2020 at 13:47)
• WLOGgery (15 messages, latest: Jun 12 2020 at 21:17)
• finite covers (20 messages, latest: Jun 12 2020 at 20:40)
• lexicographic ordering on lists (15 messages, latest: Jun 12 2020 at 17:34)
• ordered add monoids (13 messages, latest: Jun 09 2020 at 06:36)
• perfectoid spaces (62 messages, latest: Jun 08 2020 at 09:56)
• Difference between is_prime and normal (10 messages, latest: Jun 07 2020 at 13:23)
• name help (14 messages, latest: Jun 04 2020 at 14:00)
• f.g. free modules (114 messages, latest: Jun 04 2020 at 04:53)
• sign of permutation (4 messages, latest: Jun 03 2020 at 16:14)
• looping instances (3 messages, latest: Jun 02 2020 at 22:51)
• localizations (14 messages, latest: Jun 02 2020 at 18:39)
• bilinear forms (5 messages, latest: Jun 02 2020 at 18:04)
• Sheaves (149 messages, latest: Jun 02 2020 at 15:42)
• sheaves (2 messages, latest: Jun 02 2020 at 14:11)
• problem with binary biproducts (16 messages, latest: Jun 02 2020 at 12:46)
• continued fractions (2 messages, latest: Jun 01 2020 at 21:14)
• Mazur-Ulam in affine spaces (4 messages, latest: Jun 01 2020 at 18:19)
• Lean in Latex (6 messages, latest: Jun 01 2020 at 15:32)
• zmod.cast_hom (4 messages, latest: Jun 01 2020 at 06:40)
• definition of integrally closed (49 messages, latest: Jun 01 2020 at 02:54)
• A proof of Baire category theorem using #2850 (1 message, latest: May 31 2020 at 18:43)
• Finite families and map evaluation on linear m… (35 messages, latest: May 31 2020 at 15:04)
• How does norm_num check primality? (34 messages, latest: May 30 2020 at 09:50)
• need help with naming (3 messages, latest: May 30 2020 at 06:04)
• Theory of the tendsto predicate (23 messages, latest: May 29 2020 at 18:37)
• name of ring hom associated to function (8 messages, latest: May 29 2020 at 05:02)
• complex.ext_iff a simp lemma? (12 messages, latest: May 28 2020 at 14:31)
• linear algebra over semirings & semimodules (38 messages, latest: May 28 2020 at 12:02)
• rintro puzzle (14 messages, latest: May 28 2020 at 07:49)
• Fixed points of endomorphism form substructure (27 messages, latest: May 27 2020 at 16:34)
• implicit function theorem (1 message, latest: May 26 2020 at 11:48)
• Ring quotient by zero ideal. (9 messages, latest: May 25 2020 at 15:33)
• Hales 2017 Obergurgl (6 messages, latest: May 25 2020 at 04:58)
• Bundled lift for free_group (6 messages, latest: May 24 2020 at 22:58)
• How to manipulate zmod and its field structure? (6 messages, latest: May 24 2020 at 17:51)
• finite limits (24 messages, latest: May 23 2020 at 03:27)
• equivalent quadratic forms (3 messages, latest: May 21 2020 at 05:52)
• Reduction mod m (6 messages, latest: May 20 2020 at 17:39)
• (3.7 : ℝ) (38 messages, latest: May 20 2020 at 15:33)
• general_linear_group versus automorphism_group (2 messages, latest: May 20 2020 at 11:18)
• Correct phrasing of a function (17 messages, latest: May 19 2020 at 20:28)
• Ideal class group (37 messages, latest: May 19 2020 at 08:06)
• lifting arithmetic (111 messages, latest: May 19 2020 at 06:09)
• Normed spaces (171 messages, latest: May 18 2020 at 04:32)
• germs of functions (29 messages, latest: May 17 2020 at 10:33)
• of_subring as a coercion (53 messages, latest: May 15 2020 at 16:51)
• I don't understand infi (6 messages, latest: May 14 2020 at 16:06)
• Inference rule's restriction (1 message, latest: May 14 2020 at 03:53)
• group theory game (105 messages, latest: May 12 2020 at 16:25)
• groebner basis algorithm (120 messages, latest: May 12 2020 at 11:34)
• Bounded continuous functions (33 messages, latest: May 11 2020 at 18:46)
• Quotients & synthesizing (97 messages, latest: May 10 2020 at 22:32)
• quotient by zero submodule (35 messages, latest: May 10 2020 at 16:55)
• Creating limits extends reflects limits? (1 message, latest: May 10 2020 at 16:52)
• with_bot (121 messages, latest: May 09 2020 at 22:06)
• golfing challenge (60 messages, latest: May 09 2020 at 17:48)
• ring localization (10 messages, latest: May 08 2020 at 09:34)
• Equivalence of algebras (33 messages, latest: May 07 2020 at 20:36)
• from le to ge by duality? (18 messages, latest: May 07 2020 at 19:43)
• Number theory over function fields (7 messages, latest: May 07 2020 at 17:25)
• Continuity of pointwise tensor product (19 messages, latest: May 07 2020 at 16:04)
• Sqrt of 2 is irrational (9 messages, latest: May 05 2020 at 12:09)
• Define bundled homs using calc (9 messages, latest: May 05 2020 at 11:30)
• mathy may 4th (1 message, latest: May 04 2020 at 16:03)
• sober spaces (10 messages, latest: May 04 2020 at 04:36)
• Type vs Set (6 messages, latest: May 03 2020 at 09:14)
• Analytic functions (16 messages, latest: May 03 2020 at 08:36)
• linear_ordered_semiring theorems (2 messages, latest: May 03 2020 at 06:22)
• applicative ultrapower (16 messages, latest: May 02 2020 at 11:18)
• inv_neg (5 messages, latest: May 02 2020 at 11:16)
• cancel_epi (2 messages, latest: May 01 2020 at 12:29)
• push_cast and numerals (3 messages, latest: May 01 2020 at 09:41)
• linear map on basis (3 messages, latest: May 01 2020 at 06:54)
• category/ (10 messages, latest: Apr 29 2020 at 17:37)
• [finite_dimensional] (6 messages, latest: Apr 29 2020 at 14:35)
• I love coersion :).html) (5 messages, latest: Apr 28 2020 at 23:32)
• submodule map (6 messages, latest: Apr 26 2020 at 16:22)
• legendre symbols (42 messages, latest: Apr 26 2020 at 09:25)
• Coersion and composition (30 messages, latest: Apr 25 2020 at 16:19)
• finite sum (20 messages, latest: Apr 24 2020 at 07:12)
• Hedetniemi (322 messages, latest: Apr 23 2020 at 18:45)
• absurd (5 messages, latest: Apr 22 2020 at 19:44)
• how to find where the instance are define ? (9 messages, latest: Apr 22 2020 at 17:16)
• NBG (11 messages, latest: Apr 20 2020 at 12:15)
• Algebraic closure Roadmap (6 messages, latest: Apr 20 2020 at 11:27)
• bundling normal subgroups (27 messages, latest: Apr 18 2020 at 15:27)
• linear equiv constructor (25 messages, latest: Apr 18 2020 at 00:03)
• quickest way to kill "trivial mod N"? (44 messages, latest: Apr 15 2020 at 21:15)
• Lebesgue number lemma (49 messages, latest: Apr 15 2020 at 14:09)
• notations for uniform spaces (59 messages, latest: Apr 15 2020 at 11:25)
• category (195 messages, latest: Apr 15 2020 at 08:18)
• lean absurd proof (41 messages, latest: Apr 13 2020 at 09:57)
• finset.sUnion (11 messages, latest: Apr 12 2020 at 05:32)
• Dependent image (3 messages, latest: Apr 12 2020 at 01:58)
• Polynomials (47 messages, latest: Apr 11 2020 at 04:16)
• coercion from rat to a char_p field (7 messages, latest: Apr 09 2020 at 19:12)
• Ideal lemma (133 messages, latest: Apr 09 2020 at 16:03)
• mul_left_cancel (109 messages, latest: Apr 09 2020 at 09:49)
• Does classical break interval_cases? (4 messages, latest: Apr 09 2020 at 08:00)
• quanta on langlands (15 messages, latest: Apr 08 2020 at 21:57)
• squeeze_ring (18 messages, latest: Apr 08 2020 at 19:16)
• multiplication is an add_monoid_hom (7 messages, latest: Apr 08 2020 at 17:53)
• real number game (39 messages, latest: Apr 08 2020 at 15:20)
• direct limits and bundled homs (6 messages, latest: Apr 08 2020 at 07:25)
• no_zero_divisors definition (29 messages, latest: Apr 07 2020 at 09:39)
• Missing instance (2 messages, latest: Apr 06 2020 at 19:08)
• ring is slow with polynomials (41 messages, latest: Apr 06 2020 at 14:34)
• category over and under (53 messages, latest: Apr 06 2020 at 13:16)
• filter bases (40 messages, latest: Apr 06 2020 at 12:00)
• by ring is slow (6 messages, latest: Apr 06 2020 at 07:43)
• 2 = 2 (27 messages, latest: Apr 06 2020 at 05:23)
• find a term in a fintype (13 messages, latest: Apr 05 2020 at 22:56)
• filter.eventually (7 messages, latest: Apr 05 2020 at 16:47)
• unnecessary suffering in galois insertion (5 messages, latest: Apr 05 2020 at 15:13)
• Infinite sets are nonempty (6 messages, latest: Apr 05 2020 at 09:37)
• fixing subst in core (39 messages, latest: Apr 05 2020 at 09:27)
• Link between sequential and epsilon/delta versions (158 messages, latest: Apr 04 2020 at 14:46)
• Wiedijk's "Benchmark" (19 messages, latest: Apr 04 2020 at 13:56)
• Binet's Formula (4 messages, latest: Apr 04 2020 at 10:01)
• pderivative (8 messages, latest: Apr 04 2020 at 05:29)
• If some inf is a min, then the set is bounded below (12 messages, latest: Apr 03 2020 at 23:31)
• Turn a set { y : Y | exists x \in A, y = f x } into (f '' A) (30 messages, latest: Apr 03 2020 at 15:10)
• non-dependent type sheaves (11 messages, latest: Apr 02 2020 at 12:12)
• Lifting a finite set to a finset (8 messages, latest: Apr 01 2020 at 19:41)
• Borel measure space (47 messages, latest: Apr 01 2020 at 08:58)
• help proving IVT (13 messages, latest: Apr 01 2020 at 04:02)
• lattice with antiautomorphism (32 messages, latest: Mar 31 2020 at 13:09)
• strange rw behaviour with mv_polynomial (77 messages, latest: Mar 30 2020 at 16:19)
• Implicit function theorem (17 messages, latest: Mar 30 2020 at 02:06)
• nat.sqrt in lean (4 messages, latest: Mar 29 2020 at 01:10)
• mv_polynomial questions (16 messages, latest: Mar 29 2020 at 00:52)
• Density of orbits of an irrational rotation (18 messages, latest: Mar 28 2020 at 01:45)
• Speeding up Elaboration (21 messages, latest: Mar 26 2020 at 22:46)
• Bourbaki's tau (14 messages, latest: Mar 26 2020 at 20:16)
• metric_space documentation (1 message, latest: Mar 24 2020 at 20:23)
• Pigeonhole for arbitrary cardinals? (9 messages, latest: Mar 23 2020 at 20:01)
• colimits in an arbitrary equational theory (49 messages, latest: Mar 21 2020 at 22:04)
• ring_hom ≃ algebra (5 messages, latest: Mar 21 2020 at 19:06)
• Homological algebra "project" (3 messages, latest: Mar 21 2020 at 18:09)
• Category exercice (55 messages, latest: Mar 20 2020 at 17:44)
• Homological algebra (5 messages, latest: Mar 18 2020 at 11:41)
• Basic category theory observations (90 messages, latest: Mar 15 2020 at 08:08)
• long exact sequence of cohomology (100 messages, latest: Mar 14 2020 at 19:11)
• Univalence (364 messages, latest: Mar 13 2020 at 21:08)
• Bilinear forms (25 messages, latest: Mar 12 2020 at 21:38)
• "nice" group homs (10 messages, latest: Mar 12 2020 at 14:48)
• issue with bundled subgroups (196 messages, latest: Mar 10 2020 at 06:13)
• bundling subgroups – kernel (37 messages, latest: Mar 10 2020 at 04:15)
• nat.mod_mul_mod (6 messages, latest: Mar 06 2020 at 08:59)
• tendsto.nhds_congr (2 messages, latest: Mar 03 2020 at 18:57)
• Failure to halve an odd number (30 messages, latest: Mar 03 2020 at 17:38)
• log (a ^ n) = n * log a in mathlib? (105 messages, latest: Mar 03 2020 at 11:47)
• Product of univ : finset (option α) (17 messages, latest: Mar 02 2020 at 14:10)
• Collinear in incidence geometry (25 messages, latest: Mar 02 2020 at 13:18)
• 3.6.1 mathlib? (2 messages, latest: Mar 02 2020 at 11:08)
• proofs in cocalc (3 messages, latest: Mar 02 2020 at 10:33)
• zmodp (95 messages, latest: Mar 02 2020 at 08:34)
• (uniform) inducing vs embedding (9 messages, latest: Mar 02 2020 at 07:44)
• product with variable number of factors (19 messages, latest: Mar 01 2020 at 19:11)
• Euclidean geometry in mathlib? (6 messages, latest: Mar 01 2020 at 07:48)
• condensed etale cohomology (2 messages, latest: Feb 29 2020 at 23:30)
• topological space from filter (46 messages, latest: Feb 29 2020 at 21:51)
• I don't get all these types of union (8 messages, latest: Feb 29 2020 at 09:38)
• dealing with natural number subtraction (58 messages, latest: Feb 28 2020 at 06:09)
• addition in opposite (5 messages, latest: Feb 26 2020 at 18:03)
• Formalization of the statement that 0.999… = 1 (32 messages, latest: Feb 26 2020 at 17:30)
• well-ordering principle (111 messages, latest: Feb 26 2020 at 05:17)
• Zorn's Lemma (52 messages, latest: Feb 26 2020 at 00:55)
• nat case bashing (3 messages, latest: Feb 25 2020 at 17:54)
• What should be my next step here? (5 messages, latest: Feb 24 2020 at 03:51)
• proposition manipulation (53 messages, latest: Feb 24 2020 at 03:44)
• finset of coeffts of a poly (3 messages, latest: Feb 20 2020 at 16:15)
• one_ne_zero in commutative rings: funny types (24 messages, latest: Feb 19 2020 at 20:07)
• What is an automorphic representation? (12 messages, latest: Feb 19 2020 at 01:44)
• union of a finset of finsets (9 messages, latest: Feb 18 2020 at 20:14)
• finset.inter (7 messages, latest: Feb 17 2020 at 20:53)
• finite-dimensionality of field over subfield (60 messages, latest: Feb 17 2020 at 18:02)
• ⊢ S \ {s} ⊂ S (8 messages, latest: Feb 16 2020 at 18:36)
• why nonempty? (7 messages, latest: Feb 16 2020 at 12:38)
• Carlos Simpson and VHS (11 messages, latest: Feb 15 2020 at 12:05)
• class groups of number fields? (14 messages, latest: Feb 14 2020 at 16:22)
• proof basics (5 messages, latest: Feb 13 2020 at 19:33)
• subquotients (1 message, latest: Feb 13 2020 at 12:07)
• Commutative diagrams (12 messages, latest: Feb 13 2020 at 12:04)
• [h : nonempty alpha] (4 messages, latest: Feb 13 2020 at 07:47)
• Heine–Borel (7 messages, latest: Feb 13 2020 at 07:47)
• cache-olean (4 messages, latest: Feb 12 2020 at 22:02)
• Arithmetic Basics in Lean (15 messages, latest: Feb 12 2020 at 16:40)
• names? (2 messages, latest: Feb 10 2020 at 08:19)
• nonempty (24 messages, latest: Feb 10 2020 at 02:08)
• composition of algebra structures? (4 messages, latest: Feb 09 2020 at 23:03)
• "trivial" R-algebra hom construction (6 messages, latest: Feb 08 2020 at 15:03)
• bundled kernels for add_comm_groups? (9 messages, latest: Feb 06 2020 at 11:34)
• simp lemmas for matrix.mul vs has_mul.mul (11 messages, latest: Feb 05 2020 at 10:29)
• Unifying tangent_cone_at and pos_tangent_cone_at (4 messages, latest: Feb 05 2020 at 07:45)
• Cantor's intersection thm (2 messages, latest: Feb 04 2020 at 21:17)
• when does norm_num work? (29 messages, latest: Feb 01 2020 at 20:15)
• How to prove unbound_prop (9 messages, latest: Feb 01 2020 at 11:58)
• set tactic (31 messages, latest: Jan 31 2020 at 00:09)
• Conway addition thing (11 messages, latest: Jan 30 2020 at 20:05)
• irreducible top spaces (61 messages, latest: Jan 30 2020 at 15:34)
• size of a finite set (5 messages, latest: Jan 30 2020 at 14:25)
• finset puzzle (22 messages, latest: Jan 30 2020 at 14:10)
• finset.sum_add_distrib (9 messages, latest: Jan 30 2020 at 13:01)
• Inductive construction (22 messages, latest: Jan 30 2020 at 12:05)
• Combinatorics (3 messages, latest: Jan 29 2020 at 09:48)
• induction generalizing (20 messages, latest: Jan 28 2020 at 22:00)
• formal roadmaps (7 messages, latest: Jan 28 2020 at 12:14)
• Refactoring polynomials (11 messages, latest: Jan 27 2020 at 20:25)
• Algebraic geometry course (177 messages, latest: Jan 27 2020 at 12:21)
• Request for integral lemmas (8 messages, latest: Jan 26 2020 at 02:10)
• Notation for filter.eventually (2 messages, latest: Jan 25 2020 at 23:46)
• mv_polynomial puzzles (2 messages, latest: Jan 25 2020 at 13:29)
• integrals and pi (17 messages, latest: Jan 25 2020 at 01:18)
• Integrals w.r.t. non-canonical measures (25 messages, latest: Jan 23 2020 at 20:04)
• continuity of division (14 messages, latest: Jan 23 2020 at 12:06)
• linear maps over semimodule (28 messages, latest: Jan 23 2020 at 04:27)
• hello (31 messages, latest: Jan 22 2020 at 22:09)
• lie theory (13 messages, latest: Jan 21 2020 at 21:59)
• Matroids in lean (7 messages, latest: Jan 20 2020 at 20:01)
• transcendence basis (14 messages, latest: Jan 20 2020 at 19:44)
• integral domain timeout (15 messages, latest: Jan 17 2020 at 20:08)
• (∀ x : U, P x) ∨ (∀ y : V, Q y) ↔ ∀ (x : U) (y : V), P x ∨ Q (16 messages, latest: Jan 16 2020 at 15:03)
• Radical of an ideal (6 messages, latest: Jan 16 2020 at 12:29)
• proving theorems in the theory of categories (8 messages, latest: Jan 16 2020 at 05:58)
• coe_sort for finset (18 messages, latest: Jan 15 2020 at 05:33)
• filter base (9 messages, latest: Jan 14 2020 at 22:59)
• uniform convergence (3 messages, latest: Jan 14 2020 at 16:16)
• a ≤ b → f b ≤ f a (12 messages, latest: Jan 14 2020 at 13:25)
• set.not_mem_Inter_iff (9 messages, latest: Jan 13 2020 at 23:06)
• Future projects as Wiki? (1 message, latest: Jan 12 2020 at 22:27)
• formalising def of alg closed fields (5 messages, latest: Jan 12 2020 at 20:19)
• set builder notation (6 messages, latest: Jan 12 2020 at 20:14)
• compulsory pure undergraduate maths that is not in Lean (8 messages, latest: Jan 12 2020 at 00:13)
• linear independence (24 messages, latest: Jan 11 2020 at 15:44)
• | notation (2 messages, latest: Jan 11 2020 at 07:06)
• is_bounded_linear_map (9 messages, latest: Jan 08 2020 at 02:55)
• Normed algebras (1 message, latest: Jan 08 2020 at 01:45)
• Linear algebra question (4 messages, latest: Jan 07 2020 at 02:10)
• integer multiplication well-defined (5 messages, latest: Jan 06 2020 at 04:58)
• normed_ring axioms (13 messages, latest: Jan 06 2020 at 04:35)
• supr and val (4 messages, latest: Dec 30 2019 at 09:54)
• subalgebra.add_mem (6 messages, latest: Dec 23 2019 at 14:03)
• functor ext lemma? (47 messages, latest: Dec 23 2019 at 12:19)
• bundling submonoids (28 messages, latest: Dec 20 2019 at 18:39)
• field_simp fails (6 messages, latest: Dec 19 2019 at 22:25)
• Is there code for X already somewhere? (33 messages, latest: Dec 19 2019 at 18:57)
• segment partitions for integrals (56 messages, latest: Dec 18 2019 at 15:27)
• Interface for algebras (9 messages, latest: Dec 18 2019 at 13:15)
• category theory tactics (31 messages, latest: Dec 17 2019 at 05:30)
• category theory universes (12 messages, latest: Dec 16 2019 at 15:55)
• Tricky recursive proof (31 messages, latest: Dec 15 2019 at 16:27)
• Cotactic (5 messages, latest: Dec 15 2019 at 10:20)
• Jordan–Hölder for groups (2 messages, latest: Dec 13 2019 at 06:01)
• Proving physical laws (22 messages, latest: Dec 12 2019 at 09:38)
• manifolds (127 messages, latest: Dec 11 2019 at 09:17)
• Categories and Universes in Lean (33 messages, latest: Dec 08 2019 at 18:35)
• automation in category theory (13 messages, latest: Dec 07 2019 at 23:25)
• finite prods from binary prods (5 messages, latest: Dec 07 2019 at 23:23)
• tensors (4 messages, latest: Dec 07 2019 at 14:16)
• speeding up category theory (12 messages, latest: Dec 07 2019 at 11:37)
• Software verification (6 messages, latest: Dec 06 2019 at 20:36)
• compact unit ball (30 messages, latest: Dec 06 2019 at 11:24)
• filters and limits (7 messages, latest: Dec 05 2019 at 17:53)
• (Group action of) SL(n) in mathlib (5 messages, latest: Dec 05 2019 at 15:13)
• local fields / nonarchimedean fields (17 messages, latest: Dec 04 2019 at 22:49)
• normed_space timeouts (28 messages, latest: Dec 04 2019 at 19:58)
• division_ring' (4 messages, latest: Dec 04 2019 at 18:04)
• Span of finite set is sequentially closed (97 messages, latest: Dec 04 2019 at 08:59)
• Structure Theorem (15 messages, latest: Dec 01 2019 at 20:59)
• summing from 0 to n-1 (32 messages, latest: Nov 30 2019 at 12:26)
• le_nhds_of_cauchy_adhp (10 messages, latest: Nov 30 2019 at 10:01)
• constructive real algebraic numbers (25 messages, latest: Nov 29 2019 at 22:25)
• overloading \bu (16 messages, latest: Nov 29 2019 at 17:06)
• cau_seq, cauchy_seq (2 messages, latest: Nov 29 2019 at 03:12)
• omega with atoms? (6 messages, latest: Nov 28 2019 at 22:24)
• Comments? Summary of mathlib (24 messages, latest: Nov 27 2019 at 06:17)
• (non?)commutative linear ordered semirings (3 messages, latest: Nov 26 2019 at 20:16)
• analysis (86 messages, latest: Nov 24 2019 at 15:13)
• decimals in Lean (11 messages, latest: Nov 23 2019 at 16:59)
• image under smul/add/etc (3 messages, latest: Nov 21 2019 at 20:33)
• \(\[-\infty,\infty\]\) in Lean? (253 messages, latest: Nov 21 2019 at 18:22)
• Convergence uniform in one argument (12 messages, latest: Nov 20 2019 at 17:13)
• restriction of scalars (4 messages, latest: Nov 17 2019 at 16:38)
• add_comm_monoid (set M) (72 messages, latest: Nov 17 2019 at 01:12)
• pi with derivatives (1 message, latest: Nov 16 2019 at 23:50)
• one-line proof of triviality (33 messages, latest: Nov 16 2019 at 11:45)
• eigenvectors from eigenvalues (5 messages, latest: Nov 16 2019 at 10:06)
• notation for limits (4 messages, latest: Nov 16 2019 at 00:06)
• filter at_infty (45 messages, latest: Nov 15 2019 at 16:32)
• group representations (4 messages, latest: Nov 15 2019 at 01:41)
• local fields (8 messages, latest: Nov 14 2019 at 19:49)
• By schoolkid (6 messages, latest: Nov 14 2019 at 19:35)
• Define linear function from matrix (29 messages, latest: Nov 14 2019 at 17:56)
• corners (3 messages, latest: Nov 14 2019 at 08:00)
• potential projects (2 messages, latest: Nov 13 2019 at 10:36)
• norm_cast questions (4 messages, latest: Nov 13 2019 at 07:34)
• More compactness questions (7 messages, latest: Nov 12 2019 at 17:08)
• compactness and ⋃ (i : β) (H : i ∈ b) (7 messages, latest: Nov 11 2019 at 13:49)
• the integer game (18 messages, latest: Nov 10 2019 at 17:19)
• nonempty sets (8 messages, latest: Nov 09 2019 at 07:42)
• group cohomology (63 messages, latest: Nov 08 2019 at 15:10)
• Result exists? (13 messages, latest: Nov 06 2019 at 12:20)
• uniqueness of division and remainder (6 messages, latest: Nov 04 2019 at 15:49)
• lemma for noether normalization (33 messages, latest: Oct 30 2019 at 18:57)
• Proving that derivative of sin is cos (29 messages, latest: Oct 29 2019 at 10:32)
• algebra.comap (13 messages, latest: Oct 28 2019 at 06:59)
• Single Axiom for Groups (15 messages, latest: Oct 28 2019 at 00:45)
• Proof by algorithm (346 messages, latest: Oct 27 2019 at 12:08)
• algebraic independence in K-Algebras (19 messages, latest: Oct 25 2019 at 15:43)
• localization take 2 (7 messages, latest: Oct 25 2019 at 07:23)
• product of 0s and 1s (20 messages, latest: Oct 24 2019 at 00:49)
• Axiomatised summations (90 messages, latest: Oct 23 2019 at 20:48)
• physics (5 messages, latest: Oct 19 2019 at 16:48)
• constructive polynomials (25 messages, latest: Oct 19 2019 at 16:40)
• Stretch goal (4 messages, latest: Oct 18 2019 at 20:27)
• Math education question (teaching textbook proofs in Lean) (146 messages, latest: Oct 17 2019 at 22:10)
• Uniqueness of the reals (9 messages, latest: Oct 16 2019 at 08:55)
• Constructive Logic (12 messages, latest: Oct 15 2019 at 21:45)
• sensitivity project lemmas (18 messages, latest: Oct 15 2019 at 12:11)
• diamonds (7 messages, latest: Oct 14 2019 at 21:29)
• topology (41 messages, latest: Oct 12 2019 at 19:04)
• proof about sums (3 messages, latest: Oct 12 2019 at 18:10)
• ring bug? use bug? (43 messages, latest: Oct 12 2019 at 10:59)
• With Category Theory, Mathematics Escapes From Equality (40 messages, latest: Oct 12 2019 at 07:23)
• wolf goat cabbage (47 messages, latest: Oct 11 2019 at 13:59)
• analysis in Lean (9 messages, latest: Oct 11 2019 at 08:21)
• subalgebra.comm_ring (5 messages, latest: Oct 11 2019 at 00:14)
• Characterizing tendsto using sequences (5 messages, latest: Oct 10 2019 at 12:55)
• ring_hom coe (2 messages, latest: Oct 09 2019 at 21:28)
• map_nat_cast (4 messages, latest: Oct 09 2019 at 09:20)
• on real numbers (6 messages, latest: Oct 08 2019 at 09:22)
• Transitive classes for 3ʳᵈ iso thm (2 messages, latest: Oct 07 2019 at 13:53)
• dfinsupp vs finsupp (4 messages, latest: Oct 06 2019 at 21:22)
• bifunctor and End homs (1 message, latest: Sep 29 2019 at 23:58)
• Generalized Smale conjecture (24 messages, latest: Sep 29 2019 at 22:52)
• How to handle transfer to bundled homs (95 messages, latest: Sep 28 2019 at 20:09)
• Some numerology (42 messages, latest: Sep 24 2019 at 04:32)
• undone by powerful refl AI (14 messages, latest: Sep 23 2019 at 20:39)
• dirty nom_cast (4 messages, latest: Sep 23 2019 at 15:47)
• int.lt_succ_iff_le (12 messages, latest: Sep 23 2019 at 10:26)
• idiomatic statement of sandwich thm (29 messages, latest: Sep 23 2019 at 07:52)
• subgroup set coercion (29 messages, latest: Sep 20 2019 at 19:27)
• fintype or finset for integer ranges (6 messages, latest: Sep 19 2019 at 22:18)
• units and is_unit (7 messages, latest: Sep 19 2019 at 02:18)
• open embeddings (10 messages, latest: Sep 18 2019 at 14:18)
• Schroeder-Bernstein (16 messages, latest: Sep 17 2019 at 21:35)
• binary (co)products notation (25 messages, latest: Sep 12 2019 at 20:04)
• Equalizers & Products => Complete (15 messages, latest: Sep 10 2019 at 07:24)
• Lebesgue measure (11 messages, latest: Sep 09 2019 at 15:20)
• naturality (3 messages, latest: Sep 08 2019 at 17:09)
• data/rel vs logic/relation (6 messages, latest: Sep 08 2019 at 16:20)
• category universes again (41 messages, latest: Sep 08 2019 at 04:24)
• has_* limit classes (20 messages, latest: Sep 07 2019 at 13:15)
• Formalizing modern maths (10 messages, latest: Sep 06 2019 at 22:26)
• Taking the Stacks Project formalisation forward (188 messages, latest: Sep 04 2019 at 07:55)
• complementary sequences (9 messages, latest: Sep 03 2019 at 22:43)
• gluing presheaves (25 messages, latest: Sep 03 2019 at 11:36)
• Category of categories? (13 messages, latest: Aug 28 2019 at 23:41)
• sensitivity conjecture (580 messages, latest: Aug 27 2019 at 17:45)
• Travis okays sorry (2 messages, latest: Aug 26 2019 at 14:54)
• quotient_group._to_additive axiom (1 message, latest: Aug 24 2019 at 15:55)
• category_theory/groupoid and category_theory/Groupoid (5 messages, latest: Aug 23 2019 at 12:46)
• bundling mul_homs (353 messages, latest: Aug 18 2019 at 15:42)
• Formally verified factoring (9 messages, latest: Aug 16 2019 at 22:35)
• plus construction (19 messages, latest: Aug 14 2019 at 21:30)
• list.maximum should return option (6 messages, latest: Aug 12 2019 at 08:42)
• IMO problems (45 messages, latest: Aug 09 2019 at 11:14)
• characteristic predicate (3 messages, latest: Aug 07 2019 at 20:48)
• IMO2019 (69 messages, latest: Aug 06 2019 at 19:32)
• instance [semiring α] : semiring (with_zero α) (33 messages, latest: Aug 06 2019 at 17:27)
• number fields in lean? (24 messages, latest: Aug 02 2019 at 09:57)
• bundling ring_equiv (5 messages, latest: Jul 30 2019 at 19:27)
• 0 < n or n ≠ 0? (7 messages, latest: Jul 29 2019 at 16:19)
• presheafed space category (22 messages, latest: Jul 28 2019 at 10:56)
• order topology (1 message, latest: Jul 26 2019 at 12:13)
• help with sequences (15 messages, latest: Jul 24 2019 at 19:03)
• gluing functions (149 messages, latest: Jul 24 2019 at 07:40)
• colimits in Top (66 messages, latest: Jul 23 2019 at 14:03)
• One-object category (39 messages, latest: Jul 22 2019 at 02:13)
• fancy inductive types and mathematics (1 message, latest: Jul 21 2019 at 23:52)
• R^n and convex analysis (5 messages, latest: Jul 21 2019 at 18:59)
• to_additive (11 messages, latest: Jul 21 2019 at 14:52)
• has_map_add type class (4 messages, latest: Jul 21 2019 at 07:49)
• Sheafification? (24 messages, latest: Jul 20 2019 at 09:55)
• Increasing convergent subsequence (21 messages, latest: Jul 19 2019 at 18:56)
• conditionally complete linear order for nnreal (3 messages, latest: Jul 18 2019 at 17:43)
• group of fractions (12 messages, latest: Jul 17 2019 at 18:51)
• decidable_mem_of_fintype problem (31 messages, latest: Jul 17 2019 at 15:19)
• [reducible] and [irreducible] (7 messages, latest: Jul 16 2019 at 18:00)
• is_mul_hom and is_group_hom (61 messages, latest: Jul 15 2019 at 18:46)
• ring to semiring (5 messages, latest: Jul 15 2019 at 09:02)
• Weak univalence implies choice (12 messages, latest: Jul 14 2019 at 10:42)
• cache-olean instructions (14 messages, latest: Jul 11 2019 at 12:29)
• coeff_mul (47 messages, latest: Jul 11 2019 at 09:19)
• has_mul instance for option? (4 messages, latest: Jul 10 2019 at 21:43)
• measurable_coe for prob measures (30 messages, latest: Jul 08 2019 at 21:39)
• matrix inverse (78 messages, latest: Jul 08 2019 at 17:45)
• function extension (23 messages, latest: Jul 08 2019 at 16:04)
• groups (bundling etc) (41 messages, latest: Jul 08 2019 at 14:07)
• category_theory results and universes (41 messages, latest: Jul 05 2019 at 20:33)
• Maps with bounded coboundaries (1 message, latest: Jul 05 2019 at 17:06)
• making mynat an add_comm_monoid (101 messages, latest: Jul 05 2019 at 15:29)
• breaking equality with sheaves (635 messages, latest: Jul 04 2019 at 16:13)
• Integration (5 messages, latest: Jul 04 2019 at 11:51)
• Is this thing useful (67 messages, latest: Jul 03 2019 at 20:53)
• transporting measurability proofs (25 messages, latest: Jul 03 2019 at 15:45)
• categorical product (35 messages, latest: Jul 03 2019 at 08:47)
• Cauchy reals = Dedekind reals? (95 messages, latest: Jul 03 2019 at 04:45)
• order_dual disappointment (3 messages, latest: Jun 28 2019 at 18:57)
• Return type of finset.sup (10 messages, latest: Jun 28 2019 at 13:08)
• induced neighborhoods (114 messages, latest: Jun 27 2019 at 20:47)
• category_theory.category_struct.comp arguments (25 messages, latest: Jun 27 2019 at 18:23)
• Function product (19 messages, latest: Jun 26 2019 at 10:33)
• complete (distrib) lattice (24 messages, latest: Jun 26 2019 at 08:16)
• sheaves and sites (674 messages, latest: Jun 24 2019 at 12:51)
• category of discrete rings (4 messages, latest: Jun 22 2019 at 22:58)
• RFC: open immersion / embedding (5 messages, latest: Jun 21 2019 at 10:12)
• Is the Langlands program a program? (158 messages, latest: Jun 20 2019 at 01:43)
• Order on topologies (57 messages, latest: Jun 18 2019 at 08:35)
• quotient_group.map_mk (4 messages, latest: Jun 17 2019 at 15:00)
• class of primes (2 messages, latest: Jun 17 2019 at 11:06)
• group.lean in natural language (15 messages, latest: Jun 12 2019 at 16:51)
• algorithms, Fraction in library (13 messages, latest: Jun 08 2019 at 12:57)
• Hahn-Banach (15 messages, latest: Jun 07 2019 at 08:51)
• Should prime ideals be a class (11 messages, latest: Jun 07 2019 at 04:27)
• cohomology, and subgroups of subgroups (10 messages, latest: Jun 04 2019 at 07:38)
• integral rational numbers (12 messages, latest: Jun 03 2019 at 08:57)
• homotopies and stuff (3 messages, latest: Jun 01 2019 at 17:13)
• sub_mul_action (2 messages, latest: Jun 01 2019 at 14:56)
• group namespace (12 messages, latest: May 31 2019 at 18:07)
• zero group (56 messages, latest: May 31 2019 at 10:50)
• Chebyshev's inequality (6 messages, latest: May 30 2019 at 17:05)
• cubing a cube (128 messages, latest: May 29 2019 at 19:43)
• betweenness (5 messages, latest: May 29 2019 at 14:20)
• Bundled homs (52 messages, latest: May 28 2019 at 15:38)
• non-terminal simp in complex.lean (4 messages, latest: May 25 2019 at 19:19)
• Topological vector spaces (4 messages, latest: May 24 2019 at 13:30)
• topology on roption (43 messages, latest: May 24 2019 at 02:48)
• Numbers in base p (43 messages, latest: May 24 2019 at 00:00)
• Manifolds local_equiv (1 message, latest: May 22 2019 at 17:03)
• apply_rules example (69 messages, latest: May 21 2019 at 14:08)
• open subgroups (7 messages, latest: May 20 2019 at 20:18)
• ←add_assoc (8 messages, latest: May 19 2019 at 08:04)
• is_open {true} (7 messages, latest: May 16 2019 at 20:05)
• unique ring hom from ℚ (77 messages, latest: May 15 2019 at 17:24)
• cast woes (110 messages, latest: May 15 2019 at 08:31)
• representations (98 messages, latest: May 12 2019 at 12:10)
• quasicategories (6 messages, latest: May 11 2019 at 03:50)
• notations for 1 in category theory (53 messages, latest: May 10 2019 at 22:43)
• equality between natural transformations (13 messages, latest: May 07 2019 at 04:01)
• Integer gcd issues (2 messages, latest: May 06 2019 at 22:27)
• ring might be worse now? (45 messages, latest: May 04 2019 at 14:53)
• cover with property (2 messages, latest: May 01 2019 at 07:14)
• Multiple differentiability (69 messages, latest: Apr 29 2019 at 21:31)
• More examples about logic reasoning (28 messages, latest: Apr 29 2019 at 12:31)
• stuff we want (79 messages, latest: Apr 25 2019 at 17:30)
• pullback ring topology? (29 messages, latest: Apr 25 2019 at 07:39)
• linear_independent for families (91 messages, latest: Apr 24 2019 at 19:14)
• presenting a polynomial (13 messages, latest: Apr 24 2019 at 04:43)
• What is this lemma called? (19 messages, latest: Apr 23 2019 at 19:05)
• open_embedding (3 messages, latest: Apr 23 2019 at 18:15)
• how to prove simple stuffs (13 messages, latest: Apr 20 2019 at 16:26)
• what's the logic with to_additive? (12 messages, latest: Apr 18 2019 at 19:42)
• A bunch of Lean files (11 messages, latest: Apr 15 2019 at 02:13)
• preorder categories (15 messages, latest: Apr 13 2019 at 13:33)
• discontinuity of a step function (6 messages, latest: Apr 12 2019 at 21:02)
• Cute lemma (12 messages, latest: Apr 11 2019 at 21:37)
• define a function by cases (26 messages, latest: Apr 11 2019 at 18:14)
• black hole (9 messages, latest: Apr 11 2019 at 08:46)
• factoring out a constant from a linear map (11 messages, latest: Apr 10 2019 at 19:24)
• eigenvalues and eigenvectors (12 messages, latest: Apr 10 2019 at 17:37)
• Eliminating into Prop woes (3 messages, latest: Apr 09 2019 at 16:42)
• presheaves (11 messages, latest: Apr 09 2019 at 10:56)
• has_sum / has_fderiv (39 messages, latest: Apr 09 2019 at 08:44)
• has_div for groups (3 messages, latest: Apr 09 2019 at 01:36)
• inclusions of subtype.topological_space (9 messages, latest: Apr 08 2019 at 23:32)
• add_comm_subgroup (1 message, latest: Apr 08 2019 at 14:25)
• continuous functions into a topological X form an X (4 messages, latest: Apr 08 2019 at 06:56)
• binomial coefficients (77 messages, latest: Apr 08 2019 at 06:20)
• ordered commutative monoid (5 messages, latest: Apr 06 2019 at 14:56)
• induced preorder (3 messages, latest: Apr 04 2019 at 22:50)
• type class instance synthesis (22 messages, latest: Apr 04 2019 at 11:48)
• algebraic number (3 messages, latest: Apr 04 2019 at 09:16)
• equivs of mathematical objects (66 messages, latest: Apr 04 2019 at 08:00)
• matrix (11 messages, latest: Apr 03 2019 at 19:22)
• [continuity of 1/x on (0,1]](topic/continuity.20of.201.2Fx.20on.20(0.2C1.5D.html) (10 messages, latest: Apr 01 2019 at 16:42)
• locally ringed spaces in Isabelle (46 messages, latest: Apr 01 2019 at 16:29)
• condensed sets (1 message, latest: Mar 30 2019 at 23:38)
• question about game theory (106 messages, latest: Mar 29 2019 at 18:12)
• proving less than (6 messages, latest: Mar 28 2019 at 03:47)
• pow (2 messages, latest: Mar 27 2019 at 18:16)
• real examples for ring? (6 messages, latest: Mar 27 2019 at 16:44)
• finsupp.to_module (7 messages, latest: Mar 26 2019 at 19:35)
• is_ring_hom.ker (15 messages, latest: Mar 25 2019 at 13:08)
• products of linear combinations (20 messages, latest: Mar 25 2019 at 10:23)
• int.one_nonneg (21 messages, latest: Mar 25 2019 at 06:54)
• has_scalar for monoid actions (36 messages, latest: Mar 23 2019 at 14:17)
• module refactor (29 messages, latest: Mar 22 2019 at 22:36)
• Product spaces (1 message, latest: Mar 22 2019 at 20:48)
• algebra structure on lc (1 message, latest: Mar 21 2019 at 07:29)
• bounds (43 messages, latest: Mar 17 2019 at 17:11)
• topology induced by a linear order (14 messages, latest: Mar 14 2019 at 21:22)
• uniformity (5 messages, latest: Mar 12 2019 at 14:40)
• subring diamond (23 messages, latest: Mar 12 2019 at 12:16)
• topological groups/add_groups (20 messages, latest: Mar 11 2019 at 16:33)
• continuity and nhds (3 messages, latest: Mar 11 2019 at 11:58)
• inverse (14 messages, latest: Mar 10 2019 at 19:11)
• add_group.closure $ monoid_closure (8 messages, latest: Mar 10 2019 at 18:01)
• multiplicative annoyance (6 messages, latest: Mar 09 2019 at 23:41)
• non-archimedean rings (19 messages, latest: Mar 09 2019 at 21:53)
• Convexity (38 messages, latest: Mar 08 2019 at 21:14)
• Subspaces and opens (14 messages, latest: Mar 08 2019 at 19:02)
• G-modules (5 messages, latest: Mar 08 2019 at 12:05)
• out_param again (53 messages, latest: Mar 08 2019 at 09:28)
• Newton Picard (11 messages, latest: Mar 07 2019 at 21:06)
• continuous functions commute with limits v filters (19 messages, latest: Mar 07 2019 at 12:59)
• local rings (5 messages, latest: Mar 07 2019 at 08:51)
• galois theory / splitting fields (14 messages, latest: Mar 07 2019 at 08:50)
• fixed point API (7 messages, latest: Mar 05 2019 at 08:59)
• localization (3 messages, latest: Mar 05 2019 at 08:59)
• Lipschitz stuff (8 messages, latest: Mar 05 2019 at 08:29)
• product metric space (15 messages, latest: Mar 04 2019 at 18:08)
• uniform split (43 messages, latest: Mar 04 2019 at 14:10)
• lost algebraic facts (6 messages, latest: Mar 03 2019 at 18:46)
• mysterious monoid.one (6 messages, latest: Mar 03 2019 at 16:24)
• mv_polynomial (9 messages, latest: Mar 02 2019 at 22:36)
• one_iff_ker_inv (2 messages, latest: Mar 02 2019 at 14:08)
• ring hom -> unit group hom? (13 messages, latest: Mar 02 2019 at 13:30)
• Unification hints for hom (12 messages, latest: Mar 02 2019 at 10:09)
• ring confusion (9 messages, latest: Mar 01 2019 at 21:07)
• linear_independent (53 messages, latest: Feb 28 2019 at 18:10)
• hensel (5 messages, latest: Feb 28 2019 at 15:06)
• golden ratio calculation (11 messages, latest: Feb 26 2019 at 22:54)
• localization.of (10 messages, latest: Feb 26 2019 at 19:59)
• flexible indices (104 messages, latest: Feb 26 2019 at 19:23)
• quotient_group.inc (201 messages, latest: Feb 26 2019 at 16:05)
• div for (comm_)group (1 message, latest: Feb 26 2019 at 13:34)
• finite sums (119 messages, latest: Feb 24 2019 at 15:21)
• type theory for mathematicians (28 messages, latest: Feb 22 2019 at 01:16)
• defining ideals (41 messages, latest: Feb 21 2019 at 15:18)
• metric space competion (6 messages, latest: Feb 21 2019 at 08:24)
• Teaching with Lean (13 messages, latest: Feb 19 2019 at 07:45)
• free module (468 messages, latest: Feb 14 2019 at 17:16)
• kernels of quotient maps (41 messages, latest: Feb 14 2019 at 14:21)
• base change for modules (2 messages, latest: Feb 14 2019 at 05:39)
• finitely generated (sub)module (1 message, latest: Feb 13 2019 at 23:45)
• localisation of rings (38 messages, latest: Feb 13 2019 at 16:41)
• bundling functions (94 messages, latest: Feb 12 2019 at 14:47)
• ring modulo maximal (1 message, latest: Feb 12 2019 at 10:00)
• semiring polynomials (24 messages, latest: Feb 12 2019 at 07:30)
• (a * b) * c * d = (d * (b * c)) * a (5 messages, latest: Feb 11 2019 at 18:18)
• duplicate is_group_hom (2 messages, latest: Feb 11 2019 at 11:50)
• quotient classes (10 messages, latest: Feb 08 2019 at 21:26)
• floor_ring (54 messages, latest: Feb 07 2019 at 12:06)
• limits 3.0 (30 messages, latest: Feb 06 2019 at 07:50)
• a combinatorial challenge (60 messages, latest: Feb 05 2019 at 20:24)
• Inductive limits (9 messages, latest: Feb 05 2019 at 18:02)
• cardinality of integers modulo n (173 messages, latest: Feb 05 2019 at 17:24)
• card (22 messages, latest: Feb 05 2019 at 14:22)
• sub_eq_sub_of_sub_eq_sub (29 messages, latest: Feb 04 2019 at 13:12)
• digits (15 messages, latest: Feb 02 2019 at 14:31)
• groups acting on sets (6 messages, latest: Jan 31 2019 at 16:20)
• modules (7 messages, latest: Jan 30 2019 at 08:07)
• last digit challenge (15 messages, latest: Jan 29 2019 at 23:52)
• Limits of product (15 messages, latest: Jan 29 2019 at 22:34)
• nonlinarith (22 messages, latest: Jan 29 2019 at 07:44)
• adjunctions (119 messages, latest: Jan 28 2019 at 19:45)
• adding negative reals (12 messages, latest: Jan 28 2019 at 16:58)
• adding positive reals (64 messages, latest: Jan 28 2019 at 13:34)
• algebraic closure construction (12 messages, latest: Jan 24 2019 at 18:19)
• is_ring_hom left multiplication (3 messages, latest: Jan 24 2019 at 10:36)
• finset.max for nonempty sets (22 messages, latest: Jan 24 2019 at 07:13)
• Splitting topology (12 messages, latest: Jan 23 2019 at 16:14)
• multiplicative finsupp (20 messages, latest: Jan 22 2019 at 16:03)
• Long Stone-Cech (7 messages, latest: Jan 22 2019 at 12:20)
• int.cast is unique (10 messages, latest: Jan 21 2019 at 15:23)
• Zero of really small (13 messages, latest: Jan 19 2019 at 22:31)
• unique limit (2 messages, latest: Jan 19 2019 at 22:22)
• refactor functor notation (6 messages, latest: Jan 19 2019 at 00:26)
• convergent sequences are bounded (81 messages, latest: Jan 18 2019 at 20:05)
• two instances of fintype (3 messages, latest: Jan 18 2019 at 12:23)
• norm_num weirdness (34 messages, latest: Jan 18 2019 at 10:57)
• classification of finite simple groups (24 messages, latest: Jan 17 2019 at 23:03)
• div_lt_iff_lt_mul (12 messages, latest: Jan 15 2019 at 12:24)
• is_iso restate_axioms (2 messages, latest: Jan 14 2019 at 20:58)
• kernels for ring homomorphisms (8 messages, latest: Jan 14 2019 at 13:10)
• finite fields (29 messages, latest: Jan 11 2019 at 16:00)
• is_noetherian_ring (1 message, latest: Jan 11 2019 at 12:38)
• Inverse image of the indicator function (15 messages, latest: Jan 10 2019 at 09:28)
• open immersions (2 messages, latest: Jan 03 2019 at 09:02)
• Q dense in R (21 messages, latest: Dec 29 2018 at 10:01)
• comment in functor.lean (3 messages, latest: Dec 22 2018 at 06:49)
• filtered colimits (6 messages, latest: Dec 21 2018 at 22:13)
• limits 2.0 (450 messages, latest: Dec 21 2018 at 10:15)
• Bayes theorem + future directions (2 messages, latest: Dec 21 2018 at 05:28)
• uniform_continuous.continuous (17 messages, latest: Dec 20 2018 at 09:56)
• Spltting up PRs (2 messages, latest: Dec 20 2018 at 06:07)
• let in statements (4 messages, latest: Dec 19 2018 at 20:57)
• uniformity in uniform add group (1 message, latest: Dec 19 2018 at 20:12)
• over and under categories (8 messages, latest: Dec 19 2018 at 04:20)
• Ring completion (29 messages, latest: Dec 18 2018 at 17:34)
• zero ideal (16 messages, latest: Dec 17 2018 at 15:03)
• Splitting fields (110 messages, latest: Dec 17 2018 at 14:58)
• continuous_of_const (14 messages, latest: Dec 17 2018 at 11:10)
• more limit stuff (6 messages, latest: Dec 17 2018 at 05:53)
• 2 variables functions (7 messages, latest: Dec 16 2018 at 09:58)
• simple field theory (19 messages, latest: Dec 12 2018 at 18:35)
• Cantor golf (14 messages, latest: Dec 12 2018 at 18:14)
• group_hom (4 messages, latest: Dec 12 2018 at 08:40)
• closure under colimits (4 messages, latest: Dec 08 2018 at 06:04)
• weird Lean proofs (16 messages, latest: Dec 03 2018 at 19:16)
• quotients and lifts for functions of arbitrary arity (12 messages, latest: Dec 02 2018 at 17:07)
• ring requires linear order (2 messages, latest: Dec 02 2018 at 09:46)
• annoying proof challenge (12 messages, latest: Dec 01 2018 at 22:09)
• computable functions of reals (12 messages, latest: Nov 30 2018 at 16:14)
• horner polynomials (2 messages, latest: Nov 30 2018 at 09:01)
• tendsto at_top at_top (11 messages, latest: Nov 30 2018 at 07:47)
• Missing maths tactic? (64 messages, latest: Nov 25 2018 at 00:07)
• database of groups (18 messages, latest: Nov 24 2018 at 08:51)
• localisation (16 messages, latest: Nov 23 2018 at 20:54)
• simplicial complexes in lean (211 messages, latest: Nov 23 2018 at 20:31)
• module (15 messages, latest: Nov 23 2018 at 17:23)
• generalizing padic_val (75 messages, latest: Nov 23 2018 at 14:03)
• group counterexample (11 messages, latest: Nov 23 2018 at 09:16)
• Scalar multiplication not defined for functions (5 messages, latest: Nov 22 2018 at 22:01)
• is_linear_map (21 messages, latest: Nov 22 2018 at 15:37)
• Niels Henrik Module (2 messages, latest: Nov 22 2018 at 03:11)
• finsupp modules (1 message, latest: Nov 22 2018 at 02:15)
• (-1)^i (2 messages, latest: Nov 21 2018 at 19:00)
• Recursors for degree inequalities (8 messages, latest: Nov 19 2018 at 09:12)
• norm_num and fact (3 messages, latest: Nov 18 2018 at 16:31)
• should this be dec_trivial? (19 messages, latest: Nov 18 2018 at 16:01)
• decidability (49 messages, latest: Nov 17 2018 at 23:59)
• characterisation of reals (1 message, latest: Nov 17 2018 at 08:32)
• euclidean domain (19 messages, latest: Nov 15 2018 at 18:41)
• div_pos_iff_mul_pos golf (66 messages, latest: Nov 15 2018 at 16:39)
• R-Mod (2 messages, latest: Nov 15 2018 at 05:28)
• pow_lt_pow_of_lt golf (53 messages, latest: Nov 14 2018 at 16:26)
• pow_pow (4 messages, latest: Nov 14 2018 at 13:34)
• supr and range (10 messages, latest: Nov 14 2018 at 08:56)
• conv and associativity (6 messages, latest: Nov 13 2018 at 13:09)
• Gauss Lemma and Eisenstein's Criterion (6 messages, latest: Nov 13 2018 at 08:16)
• t2_space (11 messages, latest: Nov 11 2018 at 01:44)
• monoidal categories (109 messages, latest: Nov 10 2018 at 21:32)
• multivariate analysis (117 messages, latest: Nov 09 2018 at 08:42)
• sheafification (7 messages, latest: Nov 09 2018 at 04:31)
• do non-cyclic groups exist? (104 messages, latest: Nov 08 2018 at 21:06)
• parametricity (4 messages, latest: Nov 08 2018 at 10:57)
• pfilter (1 message, latest: Nov 08 2018 at 09:33)
• semimodules nein danke (113 messages, latest: Nov 08 2018 at 09:02)
• directed map (14 messages, latest: Nov 06 2018 at 16:17)
• opposite category (2 messages, latest: Nov 05 2018 at 12:45)
• Why isn't mathlib in src? (8 messages, latest: Nov 04 2018 at 21:37)
• real powers (115 messages, latest: Nov 04 2018 at 16:59)
• subring vs submodule (3 messages, latest: Nov 03 2018 at 17:45)
• has_pow for fpow (2 messages, latest: Nov 03 2018 at 13:28)
• comm_ring.closure (62 messages, latest: Oct 28 2018 at 10:29)
• with_top "diamonds" (5 messages, latest: Oct 27 2018 at 11:22)
• yoneda (276 messages, latest: Oct 23 2018 at 08:57)
• transport forever (105 messages, latest: Oct 20 2018 at 09:47)
• closure operators (1 message, latest: Oct 20 2018 at 01:56)
• discrete spaces (4 messages, latest: Oct 19 2018 at 13:54)
• weird type class issue (21 messages, latest: Oct 19 2018 at 12:22)
• ultrafilters (8 messages, latest: Oct 19 2018 at 07:17)
• Hausdorffification (38 messages, latest: Oct 19 2018 at 06:58)
• bundled bases (45 messages, latest: Oct 18 2018 at 14:36)
• extend presheaf from basis (267 messages, latest: Oct 17 2018 at 08:49)
• Hausdorff completion (24 messages, latest: Oct 15 2018 at 17:50)
• How much of analysis is formalised? (38 messages, latest: Oct 14 2018 at 20:43)
• (M1M1) Mathematical Methods in Lean (32 messages, latest: Oct 14 2018 at 13:22)
• Defining instances (22 messages, latest: Oct 13 2018 at 17:04)
• infinitary logic (1 message, latest: Oct 11 2018 at 19:51)
• top mul groups (18 messages, latest: Oct 11 2018 at 18:08)
• bicategories (18 messages, latest: Oct 10 2018 at 09:59)
• maths multivariate analysis (1 message, latest: Oct 10 2018 at 09:09)
• open_set (6 messages, latest: Oct 10 2018 at 06:07)
• to_additive multiplicative (2 messages, latest: Oct 09 2018 at 13:43)
• What's with the _ in zero_? (4 messages, latest: Oct 07 2018 at 07:43)
• is_ideal.neg_iff (8 messages, latest: Oct 06 2018 at 14:37)
• Nuances regarding naturality (23 messages, latest: Oct 05 2018 at 19:14)
• complex forms uniform space (47 messages, latest: Oct 05 2018 at 07:41)
• ordinals (12 messages, latest: Oct 04 2018 at 18:59)
• fundamental system of neighborhoods (53 messages, latest: Oct 04 2018 at 15:04)
• separated quotient (117 messages, latest: Oct 04 2018 at 06:41)
• finset sup (35 messages, latest: Oct 03 2018 at 20:18)
• Gaussian measure (8 messages, latest: Oct 02 2018 at 18:46)
• circular imports in mathlib (1 message, latest: Oct 02 2018 at 13:58)
• Compact-open topology (17 messages, latest: Oct 01 2018 at 12:51)
• Suggestions for maths/computing projects (43 messages, latest: Sep 30 2018 at 15:11)
• more int nat moans and golf plea (150 messages, latest: Sep 30 2018 at 11:36)
• complete_groups (31 messages, latest: Sep 29 2018 at 22:28)
• ideal restatement (3 messages, latest: Sep 29 2018 at 15:02)
• perm vs sym (4 messages, latest: Sep 28 2018 at 14:04)
• Separation stuff (350 messages, latest: Sep 27 2018 at 08:58)
• Continuous Functions Preserve Limits (46 messages, latest: Sep 26 2018 at 15:49)
• Uniformly Continuous on Metric Spaces (8 messages, latest: Sep 26 2018 at 13:17)
• compact spaces (4 messages, latest: Sep 22 2018 at 22:32)
• homeos (5 messages, latest: Sep 20 2018 at 20:12)
• quotient_module breakage (24 messages, latest: Sep 20 2018 at 19:39)
• Sets and boolean reflection (7 messages, latest: Sep 19 2018 at 20:02)
• physics attack (26 messages, latest: Sep 19 2018 at 13:39)
• zero in subring (1 message, latest: Sep 18 2018 at 15:13)
• transfinite compositions (14 messages, latest: Sep 17 2018 at 23:15)
• well-founded recursion & lexicographic ordering ? (7 messages, latest: Sep 14 2018 at 09:44)
• modulo group action (18 messages, latest: Sep 13 2018 at 20:27)
• connected categories (4 messages, latest: Sep 12 2018 at 17:43)
• Hensel's lemma (16 messages, latest: Sep 12 2018 at 09:09)
• matrix updates (8 messages, latest: Sep 12 2018 at 04:57)
• naive norm-num (1 message, latest: Sep 11 2018 at 14:15)
• [fX^n=0 -> f=0](topic/fX.5En.3D0.20-.3E.20f.3D0.html) (64 messages, latest: Sep 11 2018 at 12:57)
• categories (76 messages, latest: Sep 10 2018 at 02:40)
• leaking construction (18 messages, latest: Sep 10 2018 at 02:08)
• regular cardinals (94 messages, latest: Sep 09 2018 at 21:34)
• making an equiv (21 messages, latest: Sep 09 2018 at 14:04)
• degrees of polynomials (3 messages, latest: Sep 07 2018 at 11:49)
• int.coe_nat_max (2 messages, latest: Sep 06 2018 at 17:28)
• Is mathlib broken currently? (no) (10 messages, latest: Sep 06 2018 at 09:03)
• isomorphism theorems (143 messages, latest: Sep 05 2018 at 19:17)
• partial functions again (48 messages, latest: Sep 05 2018 at 07:20)
• limits notations (1 message, latest: Sep 04 2018 at 19:43)
• topological groups (1 message, latest: Sep 03 2018 at 20:23)
• is there any better way? (20 messages, latest: Sep 03 2018 at 19:01)
• how to use the pow_add theorem (22 messages, latest: Sep 03 2018 at 17:17)
• UFD (39 messages, latest: Sep 03 2018 at 04:15)
• is_group_hom a class? (4 messages, latest: Sep 02 2018 at 18:16)
• additive quotient groups? (1 message, latest: Sep 01 2018 at 20:22)
• GCD (38 messages, latest: Sep 01 2018 at 19:06)
• directed sets (4 messages, latest: Sep 01 2018 at 11:14)
• how to prove of find simple theorem (8 messages, latest: Aug 31 2018 at 20:35)
• lean-stacks-project (2 messages, latest: Aug 30 2018 at 19:53)
• 0<=d<3 implies d=0,1,2 (26 messages, latest: Aug 30 2018 at 15:40)
• Isabelle (3 messages, latest: Aug 27 2018 at 10:01)
• list of mathlib targets (62 messages, latest: Aug 26 2018 at 13:08)
• Is every complete lattice compact? (7 messages, latest: Aug 24 2018 at 07:16)
• cardinals and ordinals (11 messages, latest: Aug 22 2018 at 22:33)
• Well founded (6 messages, latest: Aug 22 2018 at 18:24)
• notation for finite free modules (5 messages, latest: Aug 22 2018 at 14:34)
• analysis refactor (26 messages, latest: Aug 22 2018 at 14:33)
• subtype instance (8 messages, latest: Aug 22 2018 at 05:25)
• filter p + fiter not p (49 messages, latest: Aug 22 2018 at 05:23)
• avoiding subtype.eq (19 messages, latest: Aug 21 2018 at 21:53)
• homology (10 messages, latest: Aug 21 2018 at 20:34)
• monotonic isomorphism between finite sets (19 messages, latest: Aug 21 2018 at 12:39)
• topology generated by an order (13 messages, latest: Aug 16 2018 at 11:10)
• Dirichlet convolution (15 messages, latest: Aug 15 2018 at 18:37)
• compact subset of hausdorff space is closed (41 messages, latest: Aug 14 2018 at 23:19)
• proving size at least 3 (23 messages, latest: Aug 14 2018 at 19:46)
• does local increasing class instance depth break mathlib rul (2 messages, latest: Aug 13 2018 at 21:24)
• norm_num question and comment (1 message, latest: Aug 13 2018 at 20:30)
• Normal submonoids (23 messages, latest: Aug 13 2018 at 10:46)
• divide by zero (3 messages, latest: Aug 11 2018 at 04:51)
• teaching use of quotients in Lean (115 messages, latest: Aug 09 2018 at 21:04)
• computable division by non-zero real (69 messages, latest: Aug 09 2018 at 18:51)
• is_homotopic_to (11 messages, latest: Aug 09 2018 at 14:07)
• reals are unique complete ordered field (90 messages, latest: Aug 09 2018 at 13:26)
• add_comm_group tactic (34 messages, latest: Aug 08 2018 at 21:38)
• d | a -> d | (a * b)? (2 messages, latest: Aug 08 2018 at 16:38)
• filter disease (29 messages, latest: Aug 08 2018 at 11:21)
• finset with two elements (13 messages, latest: Aug 08 2018 at 10:25)
• How to parse this example? (6 messages, latest: Aug 08 2018 at 00:24)
• Trivial things about convergent power series (4 messages, latest: Aug 07 2018 at 20:25)
• things to formalise (23 messages, latest: Aug 07 2018 at 20:25)
• Proving degree lemmas for polynomials (4 messages, latest: Aug 07 2018 at 20:09)
• Conjecture that Lean Prover is bivalent (1 message, latest: Aug 07 2018 at 17:12)
• ring hom induces ring hom between mv_polynomials (130 messages, latest: Aug 07 2018 at 09:47)
• ↑(m * n) = ↑m * ↑n (20 messages, latest: Aug 06 2018 at 10:41)
• partial functions on quotient (15 messages, latest: Aug 05 2018 at 18:40)
• lattice.le_sup_left' a.k.a. smileys in mathlib (22 messages, latest: Aug 05 2018 at 13:02)
• Coercions N->Z->Q->R->C (82 messages, latest: Aug 04 2018 at 18:15)
• ¬ (2 ∣ 5) (50 messages, latest: Aug 04 2018 at 06:44)
• Independent forall on nat (24 messages, latest: Aug 03 2018 at 22:35)
• order of zmod n (17 messages, latest: Aug 02 2018 at 11:35)
• sigma (8 messages, latest: Aug 01 2018 at 15:53)
• ZMOD (14 messages, latest: Aug 01 2018 at 11:01)
• int.coe_nat_mul isn't nat.cast_mul (5 messages, latest: Aug 01 2018 at 01:33)
• continuous class (12 messages, latest: Jul 30 2018 at 12:43)
• Basic finite groups (227 messages, latest: Jul 30 2018 at 07:42)
• Defining cyclic groups (31 messages, latest: Jul 29 2018 at 13:17)
• Silly function on the reals (5 messages, latest: Jul 28 2018 at 19:13)
• trash (3 messages, latest: Jul 28 2018 at 18:42)
• prime 617 challenge (23 messages, latest: Jul 28 2018 at 07:57)
• Topology - Beginner (101 messages, latest: Jul 27 2018 at 15:02)
• category theory PR (17 messages, latest: Jul 26 2018 at 13:49)
• Constructive tensor product (13 messages, latest: Jul 25 2018 at 18:26)
• products of Cauchy filters (44 messages, latest: Jul 25 2018 at 09:14)
• product topology (18 messages, latest: Jul 24 2018 at 22:43)
• delta rings (180 messages, latest: Jul 23 2018 at 17:25)
• canonical ring hom from int to R (12 messages, latest: Jul 23 2018 at 08:51)
• rings and ideals (9 messages, latest: Jul 21 2018 at 18:05)
• euclidean domains (12 messages, latest: Jul 20 2018 at 13:14)
• univeral property of quotient abelian groups (34 messages, latest: Jul 20 2018 at 11:03)
• universal properties again (40 messages, latest: Jul 19 2018 at 21:14)
• polynomial (16 messages, latest: Jul 19 2018 at 16:29)
• class vs def again (51 messages, latest: Jul 19 2018 at 14:40)
• algebra on subtypes (29 messages, latest: Jul 19 2018 at 11:48)
• classically unconstructive (1 message, latest: Jul 18 2018 at 06:09)
• constructive zerology (58 messages, latest: Jul 17 2018 at 20:14)
• extensions (26 messages, latest: Jul 16 2018 at 20:26)
• quotient topology (2 messages, latest: Jul 16 2018 at 14:14)
• Proof depending on n mod 2 (37 messages, latest: Jul 16 2018 at 12:53)
• trunc (7 messages, latest: Jul 15 2018 at 20:39)
• uniform lemma (13 messages, latest: Jul 15 2018 at 17:55)
• Explicit is_submodule (1 message, latest: Jul 14 2018 at 23:08)
• basic complex number computations (7 messages, latest: Jul 11 2018 at 15:33)
• additive group homs (184 messages, latest: Jul 10 2018 at 08:42)
• has_one for with_bot nat (1 message, latest: Jul 06 2018 at 17:38)
• atlases (100 messages, latest: Jul 02 2018 at 09:48)
• products of groups? (5 messages, latest: Jun 25 2018 at 12:21)
• image vs map and injective (13 messages, latest: Jun 25 2018 at 07:32)
• vector spaces vs modules over a field (45 messages, latest: Jun 18 2018 at 18:53)
• filters inf inf (43 messages, latest: Jun 17 2018 at 19:45)
• Transfer homomorphism (119 messages, latest: Jun 16 2018 at 10:24)
• induced, coinduced, … (30 messages, latest: Jun 15 2018 at 13:06)
• Lie algebras (42 messages, latest: Jun 13 2018 at 10:11)
• how does tactic.ring work? (4 messages, latest: Jun 13 2018 at 10:04)
• nat.pow and ring (14 messages, latest: Jun 09 2018 at 14:51)
• Model for ZFC-I in python (9 messages, latest: Jun 08 2018 at 22:39)
• computers are smart?? (6 messages, latest: Jun 05 2018 at 11:53)
• The real numbers (854 messages, latest: Jun 03 2018 at 23:03)
• travis caching (2 messages, latest: Jun 02 2018 at 02:45)
• homeomorphisms (24 messages, latest: Jun 01 2018 at 22:27)
• Cauchy-Schwarz calc (96 messages, latest: May 30 2018 at 19:14)
• Lean book for mathematicians (15 messages, latest: May 30 2018 at 14:47)
• clear_denominator (15 messages, latest: May 30 2018 at 13:14)
• LIVE CHAT: Structures for mathematicians (702 messages, latest: May 29 2018 at 21:13)
• ALEXANDRIA: Proof for the Working Mathematician (120 messages, latest: May 29 2018 at 11:46)
• ZFC equality (858 messages, latest: May 29 2018 at 09:39)
• should monotone be a class? (47 messages, latest: May 28 2018 at 21:34)
• Polynomials over a field are not quite Euclidean in lean (23 messages, latest: May 28 2018 at 19:30)
• fin n \to T vs finsupp (fin n) T (9 messages, latest: May 28 2018 at 14:26)
• affine schemes are schemes (121 messages, latest: May 28 2018 at 12:04)
• stuck on generalising finsupp.to_module (6 messages, latest: May 28 2018 at 11:52)
• minimum of finite set (62 messages, latest: May 28 2018 at 10:54)
• are quotient groups in mathlib (2 messages, latest: May 28 2018 at 10:47)
• bigop (60 messages, latest: May 28 2018 at 10:04)
• valuations (510 messages, latest: May 28 2018 at 06:40)
• nat and pnat (203 messages, latest: May 28 2018 at 04:19)
• Largest Square in the Fibonacci Sequence (717 messages, latest: May 28 2018 at 03:13)
• reductions (14 messages, latest: May 27 2018 at 22:42)
• ℤ[(1+√d)/2] (183 messages, latest: May 27 2018 at 17:00)
• strictification (9 messages, latest: May 26 2018 at 20:37)
• continuous function to pi type (67 messages, latest: May 23 2018 at 16:54)
• halting problem (23 messages, latest: May 23 2018 at 14:48)
• topological space stuff (39 messages, latest: May 23 2018 at 10:04)
• binary choice class (1 message, latest: May 23 2018 at 09:21)
• Sums over finsets (5 messages, latest: May 22 2018 at 17:20)
• bijection negation (7 messages, latest: May 17 2018 at 12:30)
• Inverse image in fin m is a finset (72 messages, latest: May 16 2018 at 15:14)
• Terence Tao's proof of Hilbert's Nullstellensatz (2 messages, latest: May 15 2018 at 20:51)
• Working with fin n (and ite?) (38 messages, latest: May 14 2018 at 19:06)
• Multiplication by n in an additive commutative group (4 messages, latest: May 14 2018 at 18:16)
• Topology on R^n (21 messages, latest: May 14 2018 at 10:02)
• open sets are unions of basis elements (55 messages, latest: May 13 2018 at 16:01)
• is continuum hypothesis true in Lean? (30 messages, latest: May 12 2018 at 00:09)
• Linear maps and module homomorphisms (8 messages, latest: May 08 2018 at 11:54)
• Univariate polynomials (151 messages, latest: May 08 2018 at 11:31)
• semiring homomorphisms (24 messages, latest: May 08 2018 at 06:14)
• Church Numeral Puzzles (217 messages, latest: May 03 2018 at 15:34)
• Writing readable uncluttered group theory (178 messages, latest: May 02 2018 at 17:47)
• quadratic reciprocity (32 messages, latest: May 01 2018 at 16:11)
• quivers and diagrams (31 messages, latest: May 01 2018 at 10:07)
• cases in term mode (31 messages, latest: May 01 2018 at 09:57)
• group actions (4 messages, latest: May 01 2018 at 06:09)
• ring tactic with homomorphism (12 messages, latest: May 01 2018 at 00:05)
• property applies to all elements of list (5 messages, latest: Apr 30 2018 at 08:22)
• naming of binary properties with left and right (5 messages, latest: Apr 30 2018 at 06:44)
• equiv and universes (8 messages, latest: Apr 29 2018 at 02:05)
• centre of partial order closed under supremum? (4 messages, latest: Apr 28 2018 at 20:28)
• category theory notations (47 messages, latest: Apr 28 2018 at 11:56)
• strange theorem (5 messages, latest: Apr 28 2018 at 05:29)
• generate filter (8 messages, latest: Apr 28 2018 at 05:19)
• When is -2 a square mod p? (48 messages, latest: Apr 28 2018 at 04:19)
• additive group game (16 messages, latest: Apr 28 2018 at 02:03)
• Left adjoint of functors between orders (2 messages, latest: Apr 27 2018 at 18:55)
• every partial order can be order-embedded into a powerset (9 messages, latest: Apr 27 2018 at 17:25)
• exponentials (4 messages, latest: Apr 27 2018 at 15:41)
• promoting equiv (137 messages, latest: Apr 27 2018 at 07:54)
• set union equality (109 messages, latest: Apr 27 2018 at 01:12)
• building mathlib (5 messages, latest: Apr 26 2018 at 09:13)
• xor is not associative (121 messages, latest: Apr 24 2018 at 16:03)
• list from a finset (47 messages, latest: Apr 19 2018 at 11:33)
• image by permutation power (105 messages, latest: Apr 17 2018 at 12:00)
• axiom of unique choice (7 messages, latest: Apr 17 2018 at 07:45)
• new is_group_hom (21 messages, latest: Apr 16 2018 at 15:30)
• burnside! (13 messages, latest: Apr 16 2018 at 07:25)
• topological space docs (251 messages, latest: Apr 16 2018 at 07:04)
• subtraction on natural numbers (26 messages, latest: Apr 11 2018 at 06:58)
• foundations of mathematics (258 messages, latest: Apr 10 2018 at 23:06)
• group acting on group (21 messages, latest: Apr 09 2018 at 13:29)
• small changes in nat and ordered groups inequalities (15 messages, latest: Apr 08 2018 at 07:54)
• easy proof of surjective_iff_injective (21 messages, latest: Apr 06 2018 at 21:01)
• homeo equiv etc. (250 messages, latest: Apr 06 2018 at 10:46)
• free group (92 messages, latest: Apr 02 2018 at 05:00)
• Easy topological space question (18 messages, latest: Apr 02 2018 at 01:23)

---

Last updated: Dec 20 2025 at 21:32 UTC