Zulip Chat Archive

Stream: Is there code for X?

---

Topics:

• Residue of the Riemann zeta function (10 messages, latest: Dec 20 2023 at 11:04)
• Cardinality of division ring generated by … (14 messages, latest: Dec 20 2023 at 09:19)
• ✔ E/L/F and K/L'/F isomorphic => \[E:L\]=\[K:L'\] (26 messages, latest: Dec 20 2023 at 01:57)
• Shifted limits (9 messages, latest: Dec 20 2023 at 00:04)
• ✔ Reasoning about CFGs (8 messages, latest: Dec 19 2023 at 23:50)
• Preorder on Option (13 messages, latest: Dec 19 2023 at 19:10)
• (infinity, 1)-categories (6 messages, latest: Dec 19 2023 at 16:07)
• Weaker statement than ContinuousSMul (4 messages, latest: Dec 19 2023 at 11:14)
• Localization and Residue Fields (6 messages, latest: Dec 19 2023 at 09:56)
• Working with big-O notation like an analyst (131 messages, latest: Dec 18 2023 at 22:08)
• Basis.localizationLocalizedModule (6 messages, latest: Dec 18 2023 at 16:14)
• Ideals for semigroups/monoids (10 messages, latest: Dec 18 2023 at 15:53)
• Set.uIoo (9 messages, latest: Dec 18 2023 at 14:52)
• Property stable under countable unions (1 message, latest: Dec 18 2023 at 09:18)
• geometric representation theory (12 messages, latest: Dec 18 2023 at 09:16)
• Basic ∀ᶠ and 𝓝 usage (11 messages, latest: Dec 18 2023 at 01:36)
• matrices (26 messages, latest: Dec 17 2023 at 22:19)
• finset sum function.extend (15 messages, latest: Dec 17 2023 at 16:35)
• rectangle is convex hull (11 messages, latest: Dec 17 2023 at 08:12)
• Complexification of a real vector space (12 messages, latest: Dec 17 2023 at 05:08)
• normSq vs Metric.ball (8 messages, latest: Dec 17 2023 at 04:31)
• Power series / bound for complex logarithm (74 messages, latest: Dec 16 2023 at 23:03)
• LinearEquiv.uniqueProd [Unique M₁] : M₁ × M₂ ≃ₗ[R] M₂ (5 messages, latest: Dec 16 2023 at 14:38)
• Inverse function theorem on manifolds (18 messages, latest: Dec 15 2023 at 22:42)
• Where is EventuallyEq.finite_iInter? (14 messages, latest: Dec 15 2023 at 20:52)
• Analysis.NormedSpace.logarithm? (5 messages, latest: Dec 15 2023 at 18:42)
• Ordered group with zero (28 messages, latest: Dec 15 2023 at 16:57)
• Catching all tactic errors (9 messages, latest: Dec 15 2023 at 10:54)
• canonical way to build Fin 3 -> a? (5 messages, latest: Dec 15 2023 at 10:42)
• acos? (3 messages, latest: Dec 15 2023 at 08:05)
• Separability degree? (85 messages, latest: Dec 13 2023 at 23:54)
• Two cyclic groups of the same order are isomorphic (49 messages, latest: Dec 13 2023 at 22:47)
• Gaussian Quadrature / Orthogonal Polynomials (2 messages, latest: Dec 13 2023 at 21:38)
• Basis.induction_on (4 messages, latest: Dec 13 2023 at 21:30)
• Fin.mulNat etc. (3 messages, latest: Dec 13 2023 at 19:48)
• ✔ Submonoid units (44 messages, latest: Dec 13 2023 at 17:55)
• loogle queries (414 messages, latest: Dec 13 2023 at 15:50)
• Degree of span of polynomials (25 messages, latest: Dec 13 2023 at 12:06)
• Every finite division ring is a field (22 messages, latest: Dec 13 2023 at 11:59)
• Lie algebra exponential map? (50 messages, latest: Dec 13 2023 at 02:23)
• Are there diagonal functors in mathlib? (5 messages, latest: Dec 12 2023 at 16:13)
• Algebra K (PerfectClosure K p) (34 messages, latest: Dec 12 2023 at 16:03)
• rw if then else (7 messages, latest: Dec 12 2023 at 09:55)
• Product of sums = sum over Pi type? (8 messages, latest: Dec 12 2023 at 07:27)
• Positivity with hypotheses (15 messages, latest: Dec 12 2023 at 07:10)
• nsmul_sInf (4 messages, latest: Dec 11 2023 at 20:25)
• Cardinality of set of sets of integers with properties. (8 messages, latest: Dec 11 2023 at 12:51)
• Continuous actions (1 message, latest: Dec 10 2023 at 22:37)
• API/tactic for subspace topology (24 messages, latest: Dec 10 2023 at 18:58)
• Tannery's theorem (11 messages, latest: Dec 10 2023 at 15:19)
• ✔ Quotient.lift but over functions with Quotient results (19 messages, latest: Dec 10 2023 at 07:51)
• Pi.group for Prop (12 messages, latest: Dec 09 2023 at 21:59)
• Should there be a ProbabilitySpace class? (178 messages, latest: Dec 09 2023 at 18:20)
• Complexity theory (349 messages, latest: Dec 09 2023 at 16:25)
• Tempered distributions (2 messages, latest: Dec 09 2023 at 07:40)
• Functional Analysis with Compact Integral Operators (3 messages, latest: Dec 09 2023 at 06:04)
• Partitions of a set (10 messages, latest: Dec 08 2023 at 19:34)
• Pi.unitEquiv (32 messages, latest: Dec 08 2023 at 18:58)
• ✔ Producing proof of length (12 messages, latest: Dec 08 2023 at 17:57)
• FunLike instance (19 messages, latest: Dec 08 2023 at 10:44)
• ✔ Cardinality of ordinals smaller than cardinal (7 messages, latest: Dec 08 2023 at 07:27)
• ✔ Overloading the propositional and /\ notation (11 messages, latest: Dec 07 2023 at 20:29)
• ✔ Simply connected set (8 messages, latest: Dec 07 2023 at 18:58)
• Dumping derivations of inductive predicate (81 messages, latest: Dec 07 2023 at 16:13)
• ✔ Greater Nat is succ of smaller (12 messages, latest: Dec 07 2023 at 12:55)
• checking a subgroup of Int is generated by an element (7 messages, latest: Dec 07 2023 at 05:40)
• BEq instance for sigma (10 messages, latest: Dec 06 2023 at 18:08)
• exists_eq_iSup_of_not_isSuccLimit (6 messages, latest: Dec 06 2023 at 15:20)
• a * b^2 = c^2 implies IsSquare a (23 messages, latest: Dec 06 2023 at 14:32)
• utf16 encoding (4 messages, latest: Dec 06 2023 at 03:29)
• docs#MeasureTheory.Measure.map_map (15 messages, latest: Dec 06 2023 at 03:22)
• Assert a structure exists with a given value for one field (6 messages, latest: Dec 05 2023 at 23:16)
• Unfolding instance notation (8 messages, latest: Dec 05 2023 at 18:32)
• The "house" of an algebraic integer (1 message, latest: Dec 05 2023 at 15:22)
• Sum notation for lists (7 messages, latest: Dec 05 2023 at 12:43)
• Is Nilpotent if a power is Nilpotent (4 messages, latest: Dec 05 2023 at 01:26)
• Pairs of distinct elements (28 messages, latest: Dec 04 2023 at 22:50)
• Ramification of infinite places (11 messages, latest: Dec 04 2023 at 08:02)
• IsClosedMap mulVec (2 messages, latest: Dec 04 2023 at 03:11)
• Fourier transforms of hermite polynomials (1 message, latest: Dec 03 2023 at 23:23)
• Power of the sum (weak Binomial theorem) (8 messages, latest: Dec 03 2023 at 21:24)
• ✔ Sum of powers (4 messages, latest: Dec 03 2023 at 19:34)
• Completeness of Rn (9 messages, latest: Dec 03 2023 at 15:05)
• Generic strong recursion over naturals (10 messages, latest: Dec 02 2023 at 20:11)
• Product of two Fintypes is a Fintype (3 messages, latest: Dec 02 2023 at 19:55)
• Filtered algebras (4 messages, latest: Dec 02 2023 at 08:40)
• specialUnitaryGroup and specialOrthogonalGroup (3 messages, latest: Dec 01 2023 at 19:54)
• L^1 as an algebra under convolution (3 messages, latest: Dec 01 2023 at 19:49)
• diameter of a ball (5 messages, latest: Dec 01 2023 at 19:46)
• (Extended) chart is a local diffeomorphism (12 messages, latest: Dec 01 2023 at 17:42)
• Ordered innerproduct spaces (4 messages, latest: Dec 01 2023 at 13:03)
• ℕ ≃ Finset ℕ (12 messages, latest: Nov 30 2023 at 20:22)
• Euler products (41 messages, latest: Nov 30 2023 at 19:48)
• ZMod lemma (21 messages, latest: Nov 30 2023 at 12:44)
• Searching doc-strings (58 messages, latest: Nov 29 2023 at 15:41)
• Multiset.sum_lt_sum (24 messages, latest: Nov 29 2023 at 11:30)
• Subgroup vs submodule (4 messages, latest: Nov 28 2023 at 13:17)
• Finsupp.sum restriction (3 messages, latest: Nov 28 2023 at 13:15)
• Going under exactly one lambda (11 messages, latest: Nov 28 2023 at 10:29)
• Proof that x \ne 0 \implies Complex.normSq \ne 0 (3 messages, latest: Nov 28 2023 at 05:44)
• Finite colimits in Action (39 messages, latest: Nov 27 2023 at 19:27)
• Embedding of PowerSeries into FormalMultivariateSeries? (1 message, latest: Nov 27 2023 at 16:06)
• Finset.InjOn.map (7 messages, latest: Nov 27 2023 at 13:15)
• Qq list (12 messages, latest: Nov 27 2023 at 09:27)
• Array.erase_data (20 messages, latest: Nov 27 2023 at 02:06)
• ✔ Transcendental, infinite lin. indep. subset, finrank=0 (5 messages, latest: Nov 26 2023 at 14:37)
• Tactic for checking all 128 cases given n : ℕ, n < 128 (2 messages, latest: Nov 26 2023 at 13:16)
• Where should mkTuple go (7 messages, latest: Nov 24 2023 at 17:07)
• Characterization of primitive elements in field extensions (5 messages, latest: Nov 24 2023 at 12:36)
• Split an equation into an OR of 2 equations (5 messages, latest: Nov 22 2023 at 17:36)
• Nat.fold with push gives an exact size (21 messages, latest: Nov 22 2023 at 16:32)
• succAbove and predAbove lemmas (8 messages, latest: Nov 22 2023 at 15:54)
• Cancellative (6 messages, latest: Nov 22 2023 at 09:33)
• ✔ For loop with Fin n (4 messages, latest: Nov 21 2023 at 23:10)
• Limits in FintypeCat (25 messages, latest: Nov 21 2023 at 22:22)
• ✔ List of pairs (12 messages, latest: Nov 21 2023 at 21:52)
• Small-step operational semantics (1 message, latest: Nov 21 2023 at 18:05)
• Product mk in category of types (1 message, latest: Nov 21 2023 at 17:18)
• Differentiability of bounded multilinear maps ? (3 messages, latest: Nov 21 2023 at 14:16)
• Filenames to Lean.Name (7 messages, latest: Nov 21 2023 at 11:58)
• Algebraic structure on lists (and/or finite tuples) (92 messages, latest: Nov 21 2023 at 10:10)
• Oriented angle is a right angle if unoriented angle is (3 messages, latest: Nov 21 2023 at 02:36)
• ✔ Splitting a UInt16 into two UInt8 (19 messages, latest: Nov 20 2023 at 21:06)
• ✔ liminf of sets (3 messages, latest: Nov 20 2023 at 08:02)
• Parser generator (3 messages, latest: Nov 20 2023 at 01:07)
• Set is open iff each point has a open neighbourhood containe (13 messages, latest: Nov 20 2023 at 00:45)
• ✔ Code review of basic proof about statically sized arrays (5 messages, latest: Nov 20 2023 at 00:10)
• Converse to Multiset.toFinset_card_of_nodup? (13 messages, latest: Nov 19 2023 at 20:58)
• Converse to Finset.equivOfCardEq (3 messages, latest: Nov 19 2023 at 20:38)
• Removing a point from a simplex (7 messages, latest: Nov 19 2023 at 12:32)
• ✔ re and im parts of integrals <-> parts of the integrand (18 messages, latest: Nov 18 2023 at 11:25)
• Algebraic Conjugate over Finite Fields (71 messages, latest: Nov 18 2023 at 07:33)
• Arzela-Ascoli for uniform spaces (21 messages, latest: Nov 18 2023 at 00:06)
• the category of sets (2 messages, latest: Nov 17 2023 at 08:02)
• Lean.Elab.Tactic.run but with multiple goals (4 messages, latest: Nov 16 2023 at 23:44)
• Galois categories (103 messages, latest: Nov 16 2023 at 22:50)
• Tensor product distributes over submodules (13 messages, latest: Nov 16 2023 at 20:20)
• Action of permutations on functions. (68 messages, latest: Nov 16 2023 at 16:27)
• simple function sum coercion (26 messages, latest: Nov 16 2023 at 10:27)
• Simp lemma for Cofan.inj (12 messages, latest: Nov 15 2023 at 18:37)
• Applying a function to a distribution (5 messages, latest: Nov 15 2023 at 15:15)
• cast from ℕ to ZMod p after adding or subtracting p (1 message, latest: Nov 15 2023 at 13:01)
• Contour Integration over the complex numbers (2 messages, latest: Nov 15 2023 at 12:51)
• Subset equal {0} of Subsingleton (6 messages, latest: Nov 15 2023 at 12:07)
• Properties of coproducts in category of types (11 messages, latest: Nov 15 2023 at 11:33)
• Exp bounded by Taylor's polynomial (1 message, latest: Nov 14 2023 at 17:27)
• bbN which le_lt or lt_le between adjacent bbNs (8 messages, latest: Nov 14 2023 at 15:24)
• Repeating probability events (3 messages, latest: Nov 14 2023 at 05:41)
• ✔ suitable choice (33 messages, latest: Nov 14 2023 at 02:25)
• ✔ Monad instance for List (7 messages, latest: Nov 14 2023 at 00:45)
• taylor expansion of determinant (3 messages, latest: Nov 13 2023 at 18:02)
• Why no explicit ContinuousWithinAt.continuousOn? (43 messages, latest: Nov 13 2023 at 15:14)
• matrix determinant lemma (149 messages, latest: Nov 13 2023 at 07:04)
• galois action is injective on roots (6 messages, latest: Nov 12 2023 at 03:10)
• Summability of g ∘ f (11 messages, latest: Nov 12 2023 at 00:03)
• [log (xy) = log x + log y for complex numbers](topic/log.20(xy).20.3D.20log.20x.20.2B.20log.20y.20for.20complex.20numbers.html) (9 messages, latest: Nov 11 2023 at 14:48)
• Transforming an expr when moving into the alts of a case (4 messages, latest: Nov 11 2023 at 10:23)
• Signed Modulo Operator (12 messages, latest: Nov 11 2023 at 03:38)
• example (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by sorry (5 messages, latest: Nov 11 2023 at 03:23)
• Combine coproducts (2 messages, latest: Nov 10 2023 at 22:32)
• Image and InjOn (21 messages, latest: Nov 10 2023 at 14:22)
• ✔ Proving equality for ideals (3 messages, latest: Nov 10 2023 at 12:46)
• A variant of Nat that has instance Zero to return 1? (5 messages, latest: Nov 10 2023 at 09:25)
• folding while mapping? (6 messages, latest: Nov 09 2023 at 00:32)
• Polynomial.degree_toFinsupp (18 messages, latest: Nov 08 2023 at 21:26)
• Coercion from finset of subtype to finset (33 messages, latest: Nov 08 2023 at 05:35)
• Product of multiplicative function on Lists (5 messages, latest: Nov 08 2023 at 04:29)
• tendsto_inv₀_cobounded (9 messages, latest: Nov 08 2023 at 04:21)
• Filter.Tendsto.exists_isBounded_image (7 messages, latest: Nov 08 2023 at 03:01)
• Struggling with List.filter (19 messages, latest: Nov 07 2023 at 07:43)
• Tactic taking a parameter (4 messages, latest: Nov 07 2023 at 01:02)
• Induction-Recursion or Universe ala Tarski? (8 messages, latest: Nov 06 2023 at 21:20)
• Distance from point in metric space to subset (10 messages, latest: Nov 06 2023 at 13:06)
• ✔ fast modulo reasoning (9 messages, latest: Nov 05 2023 at 12:53)
• Tail estimate for abs. convergent series (15 messages, latest: Nov 05 2023 at 07:44)
• Existence of Haar measure from scratch (2 messages, latest: Nov 05 2023 at 05:02)
• Homeomorphism between empty sets (in different types) (10 messages, latest: Nov 04 2023 at 12:48)
• ✔ Todd Coxeter Algorithm (5 messages, latest: Nov 04 2023 at 06:15)
• eliminating fintype (16 messages, latest: Nov 03 2023 at 17:55)
• loogle vs. HPow (4 messages, latest: Nov 03 2023 at 15:24)
• Terras Theorem (18 messages, latest: Nov 03 2023 at 08:19)
• Sorting algorithms (7 messages, latest: Nov 03 2023 at 05:42)
• Giry (1 message, latest: Nov 02 2023 at 16:49)
• ✔ Vector explicitly (5 messages, latest: Nov 02 2023 at 10:17)
• Ico_union_right (15 messages, latest: Nov 02 2023 at 06:51)
• ✔ The category A-mod (6 messages, latest: Nov 01 2023 at 23:15)
• group sum/prod in pairs even and odd summands (14 messages, latest: Nov 01 2023 at 10:53)
• DecidableEq on Multiplicative? (15 messages, latest: Nov 01 2023 at 03:46)
• surjective Pi.evalMonoidHom (3 messages, latest: Oct 31 2023 at 16:30)
• simple algebra (4 messages, latest: Oct 31 2023 at 12:36)
• ✔ nsmul distributivity (6 messages, latest: Oct 31 2023 at 10:28)
• ✔ cofactor expansion (4 messages, latest: Oct 31 2023 at 03:24)
• Tactic for proving simple inequalities (in ℕ∞) (21 messages, latest: Oct 30 2023 at 17:01)
• independent iff joint density is product (6 messages, latest: Oct 30 2023 at 08:23)
• tactic from list of tactics (3 messages, latest: Oct 29 2023 at 20:44)
• Extend a real analytic function to a complex analytic (9 messages, latest: Oct 29 2023 at 15:33)
• start induction with m = 2 (5 messages, latest: Oct 29 2023 at 14:47)
• Davenport-Schinzel sequence (1 message, latest: Oct 29 2023 at 13:03)
• (x + 1 = y) → (x % 2 == 0) ≠ (y % 2 == 0) (10 messages, latest: Oct 29 2023 at 12:24)
• output the dependencies between theorems as a directed graph (24 messages, latest: Oct 29 2023 at 07:44)
• ✔ Tactic to "unfold" abbreviature? (4 messages, latest: Oct 28 2023 at 21:28)
• ✔ Efficient and checked BFPRT/Median-of-median algorithm (5 messages, latest: Oct 28 2023 at 19:40)
• Efficient and type safe BFPRT/Median-of-median algorithm (1 message, latest: Oct 28 2023 at 17:59)
• Symmetric difference of two subgraphs (6 messages, latest: Oct 28 2023 at 17:44)
• List.dropWhile head false (9 messages, latest: Oct 28 2023 at 16:24)
• How to write proofs without knowing conclusions in advance? (22 messages, latest: Oct 28 2023 at 15:03)
• Lower bound for set bounds sInf (4 messages, latest: Oct 28 2023 at 08:01)
• machine learning with lean4 (10 messages, latest: Oct 28 2023 at 07:52)
• profinite sets (61 messages, latest: Oct 27 2023 at 22:56)
• v % 2 ≠ (v + 1) % 2 (5 messages, latest: Oct 27 2023 at 18:54)
• Finite set is union of singletons (5 messages, latest: Oct 27 2023 at 18:50)
• IntermediateField.lift_adjoin, lift_bot and lift_top (7 messages, latest: Oct 26 2023 at 22:49)
• Transform connected component into subgraph (7 messages, latest: Oct 26 2023 at 20:40)
• Approximating exp with Mclaurin polynomial (2 messages, latest: Oct 26 2023 at 19:21)
• Connected components of SimpleGraph.Subgraph (3 messages, latest: Oct 26 2023 at 13:55)
• Is x^(1/x) \leq e^(1/e) in Mathlib? (1 message, latest: Oct 26 2023 at 06:35)
• ✔ Case checking in combinatorics (11 messages, latest: Oct 25 2023 at 23:39)
• d / 2 < a implies d < 2 * a (18 messages, latest: Oct 25 2023 at 15:50)
• How to compare cardinalities of subgraph vertice sets (4 messages, latest: Oct 25 2023 at 15:41)
• The inverse of list.ofFn (7 messages, latest: Oct 24 2023 at 14:00)
• IntermediateField.mem_adjoin_iff (11 messages, latest: Oct 24 2023 at 12:11)
• Is there a linarith type tool for Nat subtraction and order (37 messages, latest: Oct 24 2023 at 07:16)
• Nontrivial closed balls are a basis (6 messages, latest: Oct 23 2023 at 22:00)
• Notion of finiteness with explicit number of elements (10 messages, latest: Oct 23 2023 at 16:01)
• Write a loop to compute elementwise cos of a FloatArray (1 message, latest: Oct 22 2023 at 23:16)
• Is there a slicker way to do "apply f to both sides"? (114 messages, latest: Oct 22 2023 at 16:43)
• Bool.beq_true and Bool.beq_false (1 message, latest: Oct 22 2023 at 12:11)
• two_smul_le_two_smul (7 messages, latest: Oct 22 2023 at 09:48)
• High 64 bits of the product of two UInt64s (1 message, latest: Oct 21 2023 at 21:13)
• Is there a field_simp variant that generates hypotheses? (16 messages, latest: Oct 21 2023 at 19:36)
• ✔ Kinda distributivity? (13 messages, latest: Oct 21 2023 at 09:44)
• Repr instance for Zsqrtd (3 messages, latest: Oct 21 2023 at 08:13)
• Simplest possible tactic implementation (3 messages, latest: Oct 21 2023 at 00:36)
• Common graphs (12 messages, latest: Oct 20 2023 at 21:12)
• AlgEquiv_invFun_apply (4 messages, latest: Oct 20 2023 at 15:35)
• [golf challenge :-(](topic/golf.20challenge.20.3A-(.html) (10 messages, latest: Oct 20 2023 at 10:07)
• Is there List.Forall₂, but for one list? (In library Std) (25 messages, latest: Oct 20 2023 at 08:45)
• subtype to type (6 messages, latest: Oct 20 2023 at 05:32)
• ✔ import mathlib or not (7 messages, latest: Oct 20 2023 at 04:00)
• exists primitive element iff finite of intermediate fields (4 messages, latest: Oct 20 2023 at 01:06)
• Extensive form games, how to formalize information sets? (4 messages, latest: Oct 19 2023 at 17:58)
• init (3 messages, latest: Oct 19 2023 at 12:53)
• Finset.range_two (8 messages, latest: Oct 19 2023 at 04:40)
• Finset iUnion (12 messages, latest: Oct 18 2023 at 14:57)
• Multiple apply (6 messages, latest: Oct 18 2023 at 14:12)
• Balls are OrdConnected (18 messages, latest: Oct 18 2023 at 07:47)
• Prove that a^2 | a for a \in \Z (16 messages, latest: Oct 18 2023 at 05:22)
• Compact elements of CPO (3 messages, latest: Oct 17 2023 at 18:29)
• loogls vs. 0 (35 messages, latest: Oct 17 2023 at 14:27)
• Should nlinarith know about x^2 \geq 0 when x is real? (19 messages, latest: Oct 17 2023 at 04:23)
• Ici (0 : Nat) = univ (7 messages, latest: Oct 16 2023 at 21:02)
• Polynomial coefficient (16 messages, latest: Oct 16 2023 at 17:49)
• ✔ Summing over a list with duplicates (58 messages, latest: Oct 16 2023 at 16:47)
• ✔ get 3 components of midpoint (3 messages, latest: Oct 16 2023 at 12:20)
• Exterior powers (15 messages, latest: Oct 16 2023 at 09:11)
• Linear projection for subsets of indices. (3 messages, latest: Oct 16 2023 at 00:24)
• basic log bounds on harmonic sums (5 messages, latest: Oct 15 2023 at 09:00)
• Defining 2-category in lean? (12 messages, latest: Oct 15 2023 at 06:01)
• golf challenge :-).html) (4 messages, latest: Oct 15 2023 at 01:36)
• How to prove sum of geometric series (8 messages, latest: Oct 14 2023 at 19:22)
• Axiomatic definition of the natural numbers (33 messages, latest: Oct 14 2023 at 11:08)
• Typeclass for nontrivial (semi)rings (6 messages, latest: Oct 14 2023 at 10:27)
• Set α × Set β ≃ Set (α ⊕ β) (32 messages, latest: Oct 14 2023 at 09:56)
• Partial Derivative of a Function (1 message, latest: Oct 12 2023 at 03:04)
• Koebe quarter theorem (11 messages, latest: Oct 11 2023 at 22:48)
• Fast Unital Ring Accumulation (13 messages, latest: Oct 10 2023 at 22:08)
• Range of a map out of Finsupp (1 message, latest: Oct 10 2023 at 13:08)
• Pattern matching syntax for Array.last/Array.pop (5 messages, latest: Oct 10 2023 at 07:56)
• tactic for assoc and comm of Finset unions and subsets (5 messages, latest: Oct 10 2023 at 06:49)
• card of sdiff and inter equals card of self (1 message, latest: Oct 10 2023 at 05:17)
• ✔ Nat.repeat with enumeration (5 messages, latest: Oct 09 2023 at 15:24)
• for … in with index (7 messages, latest: Oct 09 2023 at 12:43)
• Fintype.sum of Fintype.sum (8 messages, latest: Oct 08 2023 at 15:26)
• NormedModule ? (28 messages, latest: Oct 08 2023 at 08:52)
• Making a continuous bilinear map (19 messages, latest: Oct 08 2023 at 07:06)
• ✔ continuous and injective f : \[a, b\] → ℝ strictly mono… (8 messages, latest: Oct 08 2023 at 03:19)
• Prime number theorem (54 messages, latest: Oct 08 2023 at 01:26)
• Help proving lim_{x->inf} 1/x = 0 (50 messages, latest: Oct 07 2023 at 23:35)
• list map mem eq injective (9 messages, latest: Oct 07 2023 at 22:41)
• Direct Sums are coproducts (5 messages, latest: Oct 07 2023 at 16:45)
• Open sets are locally connected (40 messages, latest: Oct 06 2023 at 21:24)
• winding number (65 messages, latest: Oct 06 2023 at 16:06)
• First isomorphism for rings (3 messages, latest: Oct 06 2023 at 09:00)
• iUnion is compatible with product of types (4 messages, latest: Oct 05 2023 at 16:55)
• Connecting the two different sheafify (4 messages, latest: Oct 05 2023 at 14:27)
• Index from List membership? (9 messages, latest: Oct 05 2023 at 09:35)
• get arbitrary not mem of finset (9 messages, latest: Oct 05 2023 at 07:12)
• Branded Data Structure, Ghost Cell, Linearity, QTT (1 message, latest: Oct 05 2023 at 04:41)
• Sugroup sup (19 messages, latest: Oct 05 2023 at 04:29)
• Temporal Logic (6 messages, latest: Oct 04 2023 at 19:52)
• f : α × β → γ injective implies fun x ↦ f (a, x) injective (8 messages, latest: Oct 04 2023 at 16:54)
• Main Theorem of Polytope Theory (17 messages, latest: Oct 04 2023 at 00:21)
• Convert functions between subsets to functions between types (10 messages, latest: Oct 03 2023 at 09:27)
• Permutation Models (4 messages, latest: Oct 02 2023 at 13:55)
• how to ask Lean to not normalize a numeric expression? (26 messages, latest: Oct 02 2023 at 12:52)
• Refine open cover of closed interval by finite partition (1 message, latest: Oct 02 2023 at 07:19)
• Quotients equal implies related (2 messages, latest: Oct 02 2023 at 06:41)
• Countable spaces are second countable (5 messages, latest: Oct 02 2023 at 01:53)
• cons is to snoc as Fin.eq_zero_or_eq_succ is to (33 messages, latest: Oct 01 2023 at 19:56)
• ✔ How can I read a file to a string? (6 messages, latest: Oct 01 2023 at 15:34)
• Inverse of a linear map ? (24 messages, latest: Oct 01 2023 at 13:20)
• Factorial number system (xkcd 2835) (5 messages, latest: Sep 30 2023 at 20:54)
• Associated (ζₚ - 1)ᵖ⁻¹ p (11 messages, latest: Sep 29 2023 at 23:18)
• Inhabited Field (5 messages, latest: Sep 29 2023 at 17:18)
• Building a list of lists in a type with given lengths (6 messages, latest: Sep 29 2023 at 13:03)
• ✔ Instance of Nonempty (Ico (0: ℝ) 1)? (4 messages, latest: Sep 28 2023 at 08:45)
• Frobenius inner product (4 messages, latest: Sep 28 2023 at 02:52)
• ✔ Explicit inverse of bijective function (11 messages, latest: Sep 28 2023 at 02:45)
• ✔ let doc-gen4 recognize srcDir of a lean library： (14 messages, latest: Sep 27 2023 at 14:03)
• Duality principle in category theory (10 messages, latest: Sep 27 2023 at 13:03)
• Algebra.norm ℤ (8 messages, latest: Sep 27 2023 at 10:47)
• Factorisation of squarefree naturals (45 messages, latest: Sep 25 2023 at 20:38)
• Induction principles (3 messages, latest: Sep 25 2023 at 17:18)
• Cauchy Binet theorem (5 messages, latest: Sep 25 2023 at 13:58)
• Surjectivity of (ZMod m)ˣ →* (ZMod n)ˣ (3 messages, latest: Sep 24 2023 at 20:17)
• permutations preserving a function (20 messages, latest: Sep 23 2023 at 23:42)
• Sherman–Morrison formula (13 messages, latest: Sep 23 2023 at 22:07)
• float('3.3') in Lean 4? (15 messages, latest: Sep 23 2023 at 17:48)
• Noetherian hom (19 messages, latest: Sep 23 2023 at 14:48)
• noncommProd (7 messages, latest: Sep 23 2023 at 11:14)
• separable/purely inseparable extension and separable closure (9 messages, latest: Sep 23 2023 at 09:33)
• CwFs, indexed families, etc (3 messages, latest: Sep 22 2023 at 13:21)
• ✔ Continuous functions are locally bounded (4 messages, latest: Sep 21 2023 at 13:08)
• ✔ Running |_ proof as tactic (17 messages, latest: Sep 20 2023 at 12:33)
• mul as an equiv (2 messages, latest: Sep 19 2023 at 13:56)
• ✔ Not equal on inductive type (10 messages, latest: Sep 19 2023 at 10:05)
• Stolz–Cesàro theorem (7 messages, latest: Sep 18 2023 at 17:49)
• mul_left_cancel on reals (5 messages, latest: Sep 18 2023 at 17:18)
• zip with padding? (4 messages, latest: Sep 18 2023 at 11:02)
• Iterated integrals (14 messages, latest: Sep 18 2023 at 07:42)
• tensor product distributes over prod (17 messages, latest: Sep 18 2023 at 07:16)
• Continuous linear maps and quotients (2 messages, latest: Sep 17 2023 at 15:59)
• calcify tactic? (4 messages, latest: Sep 17 2023 at 15:54)
• Code Formatter (24 messages, latest: Sep 17 2023 at 07:35)
• Nowhere dense and meagre sets (41 messages, latest: Sep 16 2023 at 21:13)
• Moving a CategoryTheory.Equivalence across a Hom (25 messages, latest: Sep 15 2023 at 23:48)
• Cantor set, Cantor function? (4 messages, latest: Sep 15 2023 at 21:45)
• ✔ Subtraction for Nats (11 messages, latest: Sep 14 2023 at 20:15)
• Decidable (none ∈ L) (15 messages, latest: Sep 14 2023 at 12:55)
• Is there a non-repeating list in Init or Std? (43 messages, latest: Sep 14 2023 at 01:00)
• proofs about for loops (13 messages, latest: Sep 13 2023 at 19:01)
• ✔ nonneg of mkRat if num is nonneg (5 messages, latest: Sep 13 2023 at 15:14)
• zipWith (9 messages, latest: Sep 13 2023 at 11:29)
• Dependent vector (70 messages, latest: Sep 13 2023 at 10:52)
• Positive overlap (10 messages, latest: Sep 13 2023 at 09:58)
• Class Field Theory (11 messages, latest: Sep 12 2023 at 17:26)
• ✔ Using the intro tactic on local hypothesis (13 messages, latest: Sep 12 2023 at 06:59)
• Check if a Mac is x64 or arm64? (4 messages, latest: Sep 12 2023 at 01:52)
• Declare index for ordered array (1 message, latest: Sep 11 2023 at 20:51)
• Differences of powers (12 messages, latest: Sep 11 2023 at 18:01)
• How to get the associated attribute given membership (4 messages, latest: Sep 11 2023 at 16:14)
• Well-foundedness of product orders? (9 messages, latest: Sep 10 2023 at 09:02)
• Invertibility is an open condition for bounded linear operat (11 messages, latest: Sep 10 2023 at 08:14)
• rewrite inside a function (11 messages, latest: Sep 10 2023 at 02:20)
• Construct $\mathbb{R}^n$ and 1, infinity norms in it. (16 messages, latest: Sep 10 2023 at 02:00)
• Trace of diagonal (11 messages, latest: Sep 09 2023 at 19:34)
• A Rat is less than or eq to its ceiling (21 messages, latest: Sep 09 2023 at 19:29)
• ✔ Two Arrays are if their elements are equal (4 messages, latest: Sep 09 2023 at 13:54)
• Typeclass for 0 < n? (11 messages, latest: Sep 07 2023 at 20:29)
• Extended Euclidean Algorithm (13 messages, latest: Sep 07 2023 at 17:30)
• complex/real coercion nightmare (32 messages, latest: Sep 07 2023 at 15:28)
• ✔ sub lt add one sub (9 messages, latest: Sep 07 2023 at 06:32)
• giving a value a name, for induction (14 messages, latest: Sep 07 2023 at 03:23)
• Molecular biology (5 messages, latest: Sep 06 2023 at 09:11)
• Smallest neighborhood of a point (24 messages, latest: Sep 05 2023 at 18:16)
• Cech Cohomology (17 messages, latest: Sep 04 2023 at 20:25)
• Code for GPT-F or other LLM used for ATP (22 messages, latest: Sep 04 2023 at 07:11)
• choose an element from a fintype with positive cardinality (9 messages, latest: Sep 01 2023 at 16:06)
• Check if file exists (20 messages, latest: Sep 01 2023 at 09:38)
• card of subtype of fintype (13 messages, latest: Aug 31 2023 at 21:28)
• Set vs Subtype in Equiv.Perm (23 messages, latest: Aug 30 2023 at 22:39)
• Supremum in Subobject as a colimit (5 messages, latest: Aug 29 2023 at 23:42)
• Import position of ConstInfo (5 messages, latest: Aug 29 2023 at 21:09)
• Nat -> ZMod n -> ZMod m (5 messages, latest: Aug 29 2023 at 15:53)
• ✔ ℕ×ℕ enumeration (7 messages, latest: Aug 28 2023 at 16:46)
• Set.iUnion_inter_iUnion (4 messages, latest: Aug 28 2023 at 01:34)
• ✔ exit(status) (5 messages, latest: Aug 27 2023 at 16:53)
• congrm (9 messages, latest: Aug 27 2023 at 14:40)
• QuotientGroup.sound (7 messages, latest: Aug 26 2023 at 15:13)
• @\[pp_using_anonymous_constructor\] (3 messages, latest: Aug 26 2023 at 01:04)
• bigger range of an iUnion (10 messages, latest: Aug 25 2023 at 23:59)
• network and sockets (2 messages, latest: Aug 25 2023 at 20:25)
• remove duplicated goals? (3 messages, latest: Aug 24 2023 at 13:19)
• ✔ define map (5 messages, latest: Aug 24 2023 at 03:05)
• ✔ take out hypotheses (6 messages, latest: Aug 23 2023 at 13:06)
• MulOpposites and [instances] (7 messages, latest: Aug 23 2023 at 11:23)
• Eilenberg-moore adjunction in Mathlib? (6 messages, latest: Aug 22 2023 at 19:05)
• Sorted nonnegative tuple must have zero elements at start (18 messages, latest: Aug 22 2023 at 13:39)
• Pointwise operations on Finset (3 messages, latest: Aug 22 2023 at 11:57)
• monotone functions from finset (26 messages, latest: Aug 22 2023 at 06:53)
• (X : C) for C : Cat.{u,v} (5 messages, latest: Aug 21 2023 at 20:26)
• CharZero_of_ringChar_zero (24 messages, latest: Aug 21 2023 at 11:05)
• S-integers of a Dedekind domain is also a Dedekind domain (16 messages, latest: Aug 21 2023 at 08:21)
• NNReal subtraction is 2-Lipschitz (22 messages, latest: Aug 19 2023 at 00:03)
• Volume nonzero of nonempty interior (3 messages, latest: Aug 18 2023 at 23:01)
• Hamel basis and reals isomorphic to the complexes as an a… (3 messages, latest: Aug 18 2023 at 21:59)
• SizeOf Int (2 messages, latest: Aug 18 2023 at 17:02)
• upper semicontinuous functions are bounded below compact (47 messages, latest: Aug 18 2023 at 15:31)
• Equiv on sums with IsLeft Invariant (54 messages, latest: Aug 18 2023 at 15:17)
• finite product of infinite sums (51 messages, latest: Aug 18 2023 at 13:42)
• Commutator subgroup (aka Derived subgroup) (4 messages, latest: Aug 18 2023 at 11:10)
• Showing two expressions are not equal (9 messages, latest: Aug 17 2023 at 22:48)
• running an existing parser (2 messages, latest: Aug 17 2023 at 19:25)
• Base change for bilinear maps and quadratic forms (55 messages, latest: Aug 17 2023 at 16:37)
• Ideals in tensor product of algebras (58 messages, latest: Aug 17 2023 at 14:15)
• Intersection can be written as decreasing intersection (7 messages, latest: Aug 16 2023 at 17:38)
• ✔ Restricting codomain of an algebra homomorphism (4 messages, latest: Aug 16 2023 at 12:41)
• Finset of all functions from a fin type with image in finset (12 messages, latest: Aug 16 2023 at 07:05)
• interior of le is lt (92 messages, latest: Aug 15 2023 at 20:05)
• not singleton (2 messages, latest: Aug 15 2023 at 12:43)
• ✔ Unique Existence (9 messages, latest: Aug 15 2023 at 12:41)
• Calculating Floating Point Array with External Executable (15 messages, latest: Aug 14 2023 at 23:34)
• ✔ Fixed Field of a Normal Subgroup is Galois (7 messages, latest: Aug 14 2023 at 09:39)
• ✔ convexity of a cone (19 messages, latest: Aug 14 2023 at 08:41)
• ✔ Overwrite all textfiles in a folder (4 messages, latest: Aug 14 2023 at 06:55)
• Manipulating inequalities in ENat (26 messages, latest: Aug 14 2023 at 05:55)
• Tarski Fixed Point Theorem (9 messages, latest: Aug 11 2023 at 22:28)
• Preimage theorem (8 messages, latest: Aug 11 2023 at 17:55)
• Double opposite is the same ring/algebra (12 messages, latest: Aug 11 2023 at 14:38)
• Conjugation is bijection (10 messages, latest: Aug 11 2023 at 13:45)
• MulAction.image_iInter (12 messages, latest: Aug 11 2023 at 12:50)
• get the denominator and numerator from a rational number (7 messages, latest: Aug 11 2023 at 04:27)
• A type dependent on a value (8 messages, latest: Aug 10 2023 at 12:55)
• effect system (10 messages, latest: Aug 10 2023 at 05:21)
• Dirichlet domain (35 messages, latest: Aug 10 2023 at 03:32)
• List.range, but with Fin n as elements (2 messages, latest: Aug 09 2023 at 16:56)
• monoid instance on self maps (30 messages, latest: Aug 09 2023 at 14:30)
• Finite HasSum implies Countable support (10 messages, latest: Aug 09 2023 at 12:45)
• x^y=z from y.log(x)=log(z) (5 messages, latest: Aug 09 2023 at 12:30)
• coercion from subgroup to subset (1 message, latest: Aug 09 2023 at 10:46)
• Set over Fintype to List (5 messages, latest: Aug 09 2023 at 10:25)
• Nilpotent implies trace zero (28 messages, latest: Aug 08 2023 at 19:23)
• lemmas for getElem! (4 messages, latest: Aug 08 2023 at 14:54)
• Right exactness of tensor products (16 messages, latest: Aug 08 2023 at 13:54)
• ✔ Cross Multiplication for Fractions (13 messages, latest: Aug 08 2023 at 11:54)
• ✔ Fast innerproducts, distances? (4 messages, latest: Aug 08 2023 at 03:44)
• List.Lex is well founded on decreasing lists (13 messages, latest: Aug 07 2023 at 21:52)
• Information theory (5 messages, latest: Aug 07 2023 at 20:17)
• Expr size (7 messages, latest: Aug 07 2023 at 13:40)
• Direct sum of inner product spaces (27 messages, latest: Aug 06 2023 at 19:59)
• equivalence of fibres over equal base points? (17 messages, latest: Aug 05 2023 at 23:52)
• Calculations with presheaves (48 messages, latest: Aug 05 2023 at 23:24)
• ✔ SMul coercion for Nonneg.coeRingHom (21 messages, latest: Aug 05 2023 at 16:55)
• Ring/Semiring (11 messages, latest: Aug 05 2023 at 10:10)
• ✔ WellFoundedRelation instance on Nat x Nat (6 messages, latest: Aug 05 2023 at 06:39)
• Inner product space on α × β (56 messages, latest: Aug 05 2023 at 04:32)
• Codimension (3 messages, latest: Aug 04 2023 at 15:18)
• Measurable cardinals (1 message, latest: Aug 04 2023 at 09:58)
• [series expansion for cot piz](topic/series.20expansion.20for.20cot.20piz.html) (34 messages, latest: Aug 03 2023 at 16:20)
• String.isInfixOf (6 messages, latest: Aug 03 2023 at 12:50)
• subsingleton_of_card_eq_one (12 messages, latest: Jul 31 2023 at 21:39)
• a/b=0 in integers (5 messages, latest: Jul 31 2023 at 16:08)
• simple calculations in ZMod q (4 messages, latest: Jul 31 2023 at 08:58)
• pow_eq_zpow_mod (4 messages, latest: Jul 31 2023 at 06:39)
• Ordered finset as list (6 messages, latest: Jul 30 2023 at 08:35)
• Iterated categorical (bi/co/)products? (2 messages, latest: Jul 30 2023 at 05:54)
• Unfold projection (3 messages, latest: Jul 29 2023 at 20:35)
• A ContinuousOn version of Continuous.subtype_mk (3 messages, latest: Jul 29 2023 at 16:11)
• automorphizing (16 messages, latest: Jul 28 2023 at 22:17)
• protected alias (1 message, latest: Jul 28 2023 at 21:56)
• ✔ ∑' n, n * r ^ n (11 messages, latest: Jul 28 2023 at 13:58)
• ✔ Maps between direct sums (20 messages, latest: Jul 28 2023 at 08:14)
• Finite field is perfect ring (17 messages, latest: Jul 27 2023 at 15:20)
• Addition version of ENNReal.Lp_add_le (10 messages, latest: Jul 27 2023 at 04:45)
• DecidableRel on structures (11 messages, latest: Jul 26 2023 at 18:11)
• Partial derivatives (34 messages, latest: Jul 26 2023 at 16:38)
• ✔ HasCoproducts of ModuleCat (4 messages, latest: Jul 26 2023 at 13:31)
• Right multiplication in a monoid (12 messages, latest: Jul 25 2023 at 17:21)
• Computing the witness of an existential (9 messages, latest: Jul 25 2023 at 14:59)
• More currying of continuous multilinear maps (28 messages, latest: Jul 25 2023 at 14:32)
• ✔ unbot_le_iff? (11 messages, latest: Jul 25 2023 at 14:03)
• Finite arithmetic progressions (29 messages, latest: Jul 25 2023 at 11:48)
• ✔ tsum and HasSum (15 messages, latest: Jul 24 2023 at 20:42)
• Asymptotics of log (5 messages, latest: Jul 24 2023 at 14:24)
• ✔ limit of a bounded monotone sequence (15 messages, latest: Jul 23 2023 at 11:08)
• Compare inverses (53 messages, latest: Jul 23 2023 at 09:43)
• Fin counterpart of Nat.foldM (1 message, latest: Jul 22 2023 at 10:47)
• ✔ Using Fin n maps with n variable (5 messages, latest: Jul 21 2023 at 21:46)
• Congruum (17 messages, latest: Jul 20 2023 at 19:07)
• Tensor products of inner product spaces (23 messages, latest: Jul 20 2023 at 10:09)
• Smallest integer greater than a real (7 messages, latest: Jul 19 2023 at 21:57)
• Group isomorphisms Lean 4 (8 messages, latest: Jul 19 2023 at 17:31)
• prefunctor? (109 messages, latest: Jul 19 2023 at 16:47)
• Coprime integers can't be both zero in a non-trivial ring (25 messages, latest: Jul 19 2023 at 14:29)
• RingHom.inverse (25 messages, latest: Jul 19 2023 at 12:10)
• Characterization of ClusterPt by closure (7 messages, latest: Jul 19 2023 at 11:10)
• Primary Decomposition? (1 message, latest: Jul 18 2023 at 17:37)
• Unwrapping Option (2 messages, latest: Jul 18 2023 at 13:18)
• ✔ Showing a structure can't exist (15 messages, latest: Jul 18 2023 at 11:55)
• ✔ How do I write this set? (11 messages, latest: Jul 18 2023 at 11:55)
• Decimal expansion (7 messages, latest: Jul 18 2023 at 09:39)
• dual (4 messages, latest: Jul 17 2023 at 09:08)
• Type synonym for Nat ordered by divisibility (3 messages, latest: Jul 15 2023 at 12:35)
• help naming? (26 messages, latest: Jul 14 2023 at 20:09)
• Stochastic Optimisation (3 messages, latest: Jul 14 2023 at 18:30)
• WellFoundedLT for Fintype? (12 messages, latest: Jul 14 2023 at 14:38)
• example (a b c : α) (w : c < b) (h : b ≤ a) : a - b < a - c (7 messages, latest: Jul 14 2023 at 08:57)
• NonemptyList (6 messages, latest: Jul 14 2023 at 04:06)
• limsup_le_limsup (30 messages, latest: Jul 13 2023 at 16:49)
• Localization of modules (5 messages, latest: Jul 11 2023 at 14:45)
• padicValNat_factorial: another version of Legendre's theorem (2 messages, latest: Jul 11 2023 at 05:46)
• ✔ The only AffineSubspace with direction \bot is \bot (4 messages, latest: Jul 10 2023 at 20:38)
• Finset.prod s id (5 messages, latest: Jul 09 2023 at 17:08)
• Type of finite subsets (6 messages, latest: Jul 09 2023 at 16:09)
• Distinct variables (12 messages, latest: Jul 09 2023 at 08:00)
• Moving neighborhoods from one point to another (5 messages, latest: Jul 08 2023 at 09:48)
• Maximal suffix/prefix of list satisfying the property exists (5 messages, latest: Jul 07 2023 at 20:05)
• integrating on a piecewise differentiable curve (6 messages, latest: Jul 07 2023 at 17:50)
• Coprime if product is squarefree (14 messages, latest: Jul 07 2023 at 15:25)
• get the lastDrop (3 messages, latest: Jul 07 2023 at 08:36)
• 0 ≤ b → ((a / b : ℤ) : ℚ) ≤ (a / b : ℚ) (6 messages, latest: Jul 06 2023 at 07:45)
• Eta reduction for structures (15 messages, latest: Jul 05 2023 at 00:06)
• Partial sums (12 messages, latest: Jul 04 2023 at 21:40)
• Product and coproduct in the opposite category (6 messages, latest: Jul 04 2023 at 21:31)
• EMetric instance on ENNReal (17 messages, latest: Jul 03 2023 at 19:33)
• Finding iteration satisfying a predicate in option if exists (3 messages, latest: Jul 03 2023 at 02:40)
• Not-implemented exception? (3 messages, latest: Jul 03 2023 at 02:01)
• not_dvd_pow_sub_one (17 messages, latest: Jul 02 2023 at 22:39)
• Nat.coprime (1 message, latest: Jul 02 2023 at 19:50)
• prove instance equality (5 messages, latest: Jul 02 2023 at 19:39)
• ✔ Round trip transport (7 messages, latest: Jul 02 2023 at 15:18)
• ✔ The group of endomorphisms of an object in a groupoid (4 messages, latest: Jul 02 2023 at 05:41)
• x<1 if geometric progression converges (7 messages, latest: Jul 01 2023 at 23:14)
• ✔ forall_congr but for TFAE (13 messages, latest: Jun 30 2023 at 13:44)
• ✔ Cardinality of a set (8 messages, latest: Jun 30 2023 at 07:41)
• pi/2 + 2pi k (19 messages, latest: Jun 30 2023 at 02:46)
• Q/Z and cyclic subgroups (4 messages, latest: Jun 29 2023 at 20:15)
• How do I call (p : Prop) when defining Decidable p? (4 messages, latest: Jun 29 2023 at 08:00)
• ✔ Find where a term was declared (13 messages, latest: Jun 28 2023 at 18:36)
• ✔ Fubini for finsum (8 messages, latest: Jun 28 2023 at 17:26)
• Well-ordering of the integers (11 messages, latest: Jun 28 2023 at 16:19)
• tactic for easy calculations in ZMod p? (62 messages, latest: Jun 28 2023 at 12:33)
• Nontrivial term of nontrivial type (5 messages, latest: Jun 27 2023 at 18:52)
• Metaprogramming a structure declaration (35 messages, latest: Jun 26 2023 at 22:44)
• ✔ "Fail" and "assert" commands? (8 messages, latest: Jun 26 2023 at 03:40)
• Tangent space to a functor (1 message, latest: Jun 25 2023 at 12:14)
• Bound on ln (natural log) (5 messages, latest: Jun 25 2023 at 10:02)
• ✔ tactic for matching cases of nested induction (4 messages, latest: Jun 25 2023 at 05:28)
• Moebius Inversion on a subset of ℕ (11 messages, latest: Jun 24 2023 at 10:18)
• setoid "glue this set into a pt" (13 messages, latest: Jun 23 2023 at 18:07)
• ✔ Multiple of summable function is summable (6 messages, latest: Jun 22 2023 at 09:52)
• ✔ card_subroup_le_card_group (6 messages, latest: Jun 21 2023 at 22:16)
• conditional iff (6 messages, latest: Jun 21 2023 at 19:41)
• Right action equals left action (13 messages, latest: Jun 21 2023 at 16:57)
• ENNReal.mul_div (33 messages, latest: Jun 21 2023 at 09:17)
• ✔ continuity of fun c ↦ ContinuousMap.mk fun x ↦ c • x (4 messages, latest: Jun 21 2023 at 00:19)
• evaluation of power series (13 messages, latest: Jun 20 2023 at 15:29)
• Simplifying transpose of a matrix (25 messages, latest: Jun 19 2023 at 21:05)
• equating numbers from maps and co maps (5 messages, latest: Jun 19 2023 at 19:50)
• ✔ Convert subgroup of subgroup (4 messages, latest: Jun 19 2023 at 01:22)
• ✔ Finset.union_singleton? (7 messages, latest: Jun 19 2023 at 00:57)
• ✔ defining cartesian product (29 messages, latest: Jun 18 2023 at 16:58)
• pAdicValTR (4 messages, latest: Jun 16 2023 at 20:56)
• Derivative offset by a constant (9 messages, latest: Jun 16 2023 at 13:06)
• ✔ simple fact (3 messages, latest: Jun 15 2023 at 06:44)
• Every complete linear order is a compl. distributive lattice (3 messages, latest: Jun 14 2023 at 21:08)
• open interval in nonempty open set (4 messages, latest: Jun 13 2023 at 22:34)
• measure_theory.integrable uncurry f (5 messages, latest: Jun 13 2023 at 14:50)
• filter.at_top for intervals (14 messages, latest: Jun 13 2023 at 01:01)
• integral of a function of norm (4 messages, latest: Jun 12 2023 at 22:44)
• Boundedness Theorem for Continuous Functions (10 messages, latest: Jun 12 2023 at 16:28)
• Zero rank iff zero matrix (33 messages, latest: Jun 12 2023 at 00:51)
• Integration on ℝ by parts (15 messages, latest: Jun 11 2023 at 13:54)
• ✔ Modular arithmetic fact (12 messages, latest: Jun 11 2023 at 06:13)
• ✔ m=0 proof (5 messages, latest: Jun 10 2023 at 21:24)
• Making a computable version of MvPolynomial.monomial (25 messages, latest: Jun 10 2023 at 10:31)
• Formalization of algorithms? (2 messages, latest: Jun 10 2023 at 07:51)
• Perm on the other side of sublist (20 messages, latest: Jun 10 2023 at 07:26)
• Markov chains ? (13 messages, latest: Jun 09 2023 at 17:40)
• ✔ Extending a lin indep set by picking elements from a sp… (51 messages, latest: Jun 08 2023 at 12:46)
• Probability Distributions (47 messages, latest: Jun 07 2023 at 20:39)
• Rank of Matrix Multiplied by an Invertible Matrix (11 messages, latest: Jun 07 2023 at 13:53)
• Single line json formatting (5 messages, latest: Jun 07 2023 at 02:33)
• Get projection functions for constructors (5 messages, latest: Jun 05 2023 at 05:24)
• Finset for computation (3 messages, latest: Jun 05 2023 at 04:01)
• Cardinality of the type of linear orders on a fintype (7 messages, latest: May 31 2023 at 14:15)
• presentable objects (4 messages, latest: May 30 2023 at 11:05)
• HOrElse for lists (5 messages, latest: May 30 2023 at 10:15)
• Dependency graph for Lean4 project (2 messages, latest: May 29 2023 at 12:09)
• Rewriting constructors under forall bindings (24 messages, latest: May 29 2023 at 02:54)
• ✔ Functions that return α (7 messages, latest: May 28 2023 at 17:07)
• ✔ How do I invoke a theorem inside a definition? (7 messages, latest: May 28 2023 at 16:44)
• ✔ Casting types (10 messages, latest: May 28 2023 at 13:45)
• Tensor products (52 messages, latest: May 28 2023 at 12:29)
• ✔ cast of types with has_coe (4 messages, latest: May 28 2023 at 10:33)
• Equivalence-invariance of constructions on categories (8 messages, latest: May 28 2023 at 02:01)
• ✔ How do I use Fin.lt? (5 messages, latest: May 27 2023 at 11:00)
• derivative commutes with infinite sum (8 messages, latest: May 26 2023 at 22:10)
• Multiplication distributes across integrals (51 messages, latest: May 26 2023 at 19:13)
• filter tendsto limit from left right top bottom (5 messages, latest: May 26 2023 at 18:32)
• Multiple dimension (28 messages, latest: May 26 2023 at 17:59)
• ✔ Shifting an integral (16 messages, latest: May 24 2023 at 22:59)
• quotient.lift_on_family (36 messages, latest: May 23 2023 at 15:26)
• Sum of a multiplicative subgroup of a field is zero (28 messages, latest: May 21 2023 at 20:59)
• Preferred spelling of p-adic valuation? (6 messages, latest: May 20 2023 at 19:58)
• norm of units (4 messages, latest: May 20 2023 at 10:55)
• Ring hom ℤ/nℤ → ℤ/mℤ? (27 messages, latest: May 20 2023 at 09:24)
• Jointly Epimorphic Families (1 message, latest: May 19 2023 at 18:12)
• Finite product of modules is a coproduct (22 messages, latest: May 19 2023 at 15:56)
• Star-semilinear maps are semilinear when star is trivial (54 messages, latest: May 19 2023 at 07:45)
• Notation for sets parametrized (3 messages, latest: May 18 2023 at 20:40)
• Derivative commutes with conjugation (4 messages, latest: May 18 2023 at 19:10)
• ✔ tactic for trivial things related to Nat, < and ≤ (35 messages, latest: May 18 2023 at 17:19)
• adjunctions in bicategories (8 messages, latest: May 18 2023 at 01:29)
• ✔ if then else with negation in premises (12 messages, latest: May 16 2023 at 16:56)
• unfold tactic without requiring names (5 messages, latest: May 15 2023 at 04:38)
• ✔ Binomial distribution (4 messages, latest: May 14 2023 at 13:17)
• Proving Pell's equation is solvable (119 messages, latest: May 14 2023 at 11:08)
• Schwarz–Milnor lemma (8 messages, latest: May 14 2023 at 08:26)
• Double factorials (29 messages, latest: May 12 2023 at 07:36)
• Simplify lambda expressions (16 messages, latest: May 11 2023 at 17:59)
• Monadic operations inside List.takeWhile (8 messages, latest: May 10 2023 at 19:26)
• Pulling lets to the outside of a statement (13 messages, latest: May 10 2023 at 18:59)
• ✔ Order extension principle (9 messages, latest: May 10 2023 at 18:52)
• Measurability of euclidean space (17 messages, latest: May 10 2023 at 18:23)
• Quoting a TSepArray (9 messages, latest: May 09 2023 at 15:59)
• meet-irreducible element (5 messages, latest: May 08 2023 at 12:38)
• Connected, but not path-connected space (4 messages, latest: May 07 2023 at 14:22)
• pattern matching on vectors (1 message, latest: May 06 2023 at 07:32)
• ✔ vector equivalent of list.map_eq_map_iff (6 messages, latest: May 06 2023 at 07:32)
• Induced discrete topology (5 messages, latest: May 05 2023 at 13:26)
• set of equivalences classes is equiv to quotient (22 messages, latest: May 05 2023 at 08:27)
• Finiteness of zeta function (4 messages, latest: May 05 2023 at 05:30)
• monotone sequence that tends to infinity (6 messages, latest: May 02 2023 at 09:03)
• Stone duality (5 messages, latest: Apr 30 2023 at 17:23)
• Rewrite all instances of a type (35 messages, latest: Apr 30 2023 at 17:00)
• ✔ Decidable Forall (3 messages, latest: Apr 30 2023 at 08:06)
• action of Galois groups / "univalence" / auto-generate thms? (39 messages, latest: Apr 27 2023 at 15:30)
• Discrete Functions / Maps (6 messages, latest: Apr 27 2023 at 09:41)
• Restricted Monads (33 messages, latest: Apr 27 2023 at 04:17)
• ✔ Search in lean4? (9 messages, latest: Apr 26 2023 at 21:14)
• ✔ Heterogeneous equality and dependent pairs (5 messages, latest: Apr 26 2023 at 07:43)
• a chain related by ≤ and a chain related by < (7 messages, latest: Apr 25 2023 at 18:07)
• function equal to id of function (norm iterated_fderiv) (2 messages, latest: Apr 25 2023 at 13:35)
• ✔ Axiom of choice on countable types (21 messages, latest: Apr 24 2023 at 08:23)
• converse to docs#set.countable_univ (3 messages, latest: Apr 24 2023 at 07:28)
• Existence of a TM (or other) for computable lean functions (32 messages, latest: Apr 23 2023 at 09:01)
• ✔ is there a binterᵢ_nat_prev_inter_binterᵢ (7 messages, latest: Apr 21 2023 at 13:43)
• ✔ Deque data type (10 messages, latest: Apr 20 2023 at 11:25)
• ✔ Dependent pair type (4 messages, latest: Apr 20 2023 at 10:06)
• Nat.mul_lt_mul0 (7 messages, latest: Apr 20 2023 at 09:42)
• relabeling Fin n (7 messages, latest: Apr 19 2023 at 21:19)
• ✔ additive implies linear / Cauchy's equation for ℤ (7 messages, latest: Apr 19 2023 at 14:09)
• ✔ Infinite Periodicity (15 messages, latest: Apr 18 2023 at 05:16)
• Brouwer's fixed point theorem (4 messages, latest: Apr 16 2023 at 21:00)
• Notations in Differential Geometry (2 messages, latest: Apr 16 2023 at 09:34)
• Iff not (9 messages, latest: Apr 13 2023 at 20:50)
• Comparing UInt64 and Nat (3 messages, latest: Apr 12 2023 at 17:50)
• Formalising Commutative Algebra (9 messages, latest: Apr 12 2023 at 12:59)
• back? tactic (14 messages, latest: Apr 11 2023 at 20:17)
• Rado's theorem on matroids (45 messages, latest: Apr 10 2023 at 19:49)
• subfamilies are linearly independent (16 messages, latest: Apr 09 2023 at 19:27)
• Alternating sum over powerset and decidable instances (18 messages, latest: Apr 08 2023 at 21:15)
• Transport a partial_order instance? (3 messages, latest: Apr 07 2023 at 19:54)
• ✔ uniqueness of quotient remainder (6 messages, latest: Apr 06 2023 at 21:14)
• Monodromy theorem (4 messages, latest: Apr 05 2023 at 21:58)
• Canonical injection into the localization (42 messages, latest: Apr 05 2023 at 07:30)
• lean 4 ac_refl (10 messages, latest: Apr 04 2023 at 14:18)
• Algebraic closure is normal (3 messages, latest: Apr 04 2023 at 09:58)
• ✔ dedekind domain and ring equivalences (11 messages, latest: Apr 03 2023 at 09:46)
• ✔ Even and odd induction (8 messages, latest: Apr 01 2023 at 18:37)
• If Fintype α then Fintype (Finset α) (4 messages, latest: Apr 01 2023 at 14:29)
• category of pro-objects (27 messages, latest: Mar 31 2023 at 14:14)
• Summing over pairs (13 messages, latest: Mar 28 2023 at 14:29)
• equiv from fin n coming from card = n (8 messages, latest: Mar 28 2023 at 12:25)
• ✔ polynomial.eval_at_zero (12 messages, latest: Mar 24 2023 at 22:22)
• Closedness is a local property (17 messages, latest: Mar 24 2023 at 19:26)
• norm of a linear map from R (6 messages, latest: Mar 24 2023 at 03:25)
• iff imp distrib (3 messages, latest: Mar 23 2023 at 20:14)
• Check if s is a substring of t (3 messages, latest: Mar 23 2023 at 11:22)
• filter.eventually_pi (7 messages, latest: Mar 23 2023 at 11:17)
• function to take every nth element from a List? (5 messages, latest: Mar 22 2023 at 21:27)
• Profunctors (2 messages, latest: Mar 22 2023 at 19:03)
• ✔ Finset of every permutation list given a Finset (5 messages, latest: Mar 22 2023 at 13:05)
• X_i divides f if f=0 when X_i=0 (12 messages, latest: Mar 22 2023 at 12:40)
• algebra.adjoin API (5 messages, latest: Mar 20 2023 at 19:13)
• Lemmas for maps on finsets (3 messages, latest: Mar 20 2023 at 17:50)
• Generalized Isomorphism Theorem (9 messages, latest: Mar 20 2023 at 12:31)
• set on a subtype as set on the type? (17 messages, latest: Mar 19 2023 at 20:08)
• Z i ⊆ ∑ j in I, Z j (7 messages, latest: Mar 19 2023 at 19:19)
• is_submodule ? (41 messages, latest: Mar 19 2023 at 00:33)
• ✔ well-founded lt on bounded-below integers (16 messages, latest: Mar 18 2023 at 12:13)
• ✔ real.cos and real.sin as infinite series (43 messages, latest: Mar 13 2023 at 18:02)
• Groups with negation and linear order? (8 messages, latest: Mar 13 2023 at 17:11)
• Reading a file (5 messages, latest: Mar 13 2023 at 15:29)
• element of nonempty set with smallest height (11 messages, latest: Mar 13 2023 at 14:06)
• transform fun a => f a back to f? (3 messages, latest: Mar 13 2023 at 11:54)
• lean 4: minimal by (9 messages, latest: Mar 12 2023 at 17:05)
• Proving Simple Lemma for Lists (7 messages, latest: Mar 10 2023 at 17:37)
• ✔ Lean 4: checking if a string is a substring of another (11 messages, latest: Mar 10 2023 at 08:22)
• returning a unique element given a Finset of card = 1 (10 messages, latest: Mar 09 2023 at 12:20)
• Odd number mod eight (37 messages, latest: Mar 08 2023 at 22:34)
• Riemann series theorem? (35 messages, latest: Mar 08 2023 at 08:30)
• An infinite integral has positive infinite support (3 messages, latest: Mar 05 2023 at 19:17)
• ✔ definition for lambda sugar (5 messages, latest: Mar 05 2023 at 11:12)
• ✔ Group with negation? (3 messages, latest: Mar 05 2023 at 02:36)
• Residue field of a prime is finite (6 messages, latest: Mar 04 2023 at 22:23)
• ✔ metric instance out of emetric one? (15 messages, latest: Mar 01 2023 at 15:10)
• pow_X_dvd_iff (8 messages, latest: Mar 01 2023 at 14:24)
• Master Theorem (15 messages, latest: Feb 26 2023 at 23:05)
• odd prime at least three (8 messages, latest: Feb 26 2023 at 12:38)
• symmetry tactic for not equals (17 messages, latest: Feb 25 2023 at 21:42)
• Measurability of units multiplication (5 messages, latest: Feb 25 2023 at 09:19)
• Euler's Theorem (23 messages, latest: Feb 24 2023 at 07:14)
• Exact absurd (10 messages, latest: Feb 22 2023 at 18:52)
• ✔ normed_linear_ordered_field (11 messages, latest: Feb 22 2023 at 17:34)
• list.map_id' with weaker hypothesis (19 messages, latest: Feb 21 2023 at 17:29)
• ✔ Show de Brujin indices when using #print (3 messages, latest: Feb 21 2023 at 12:01)
• Idiomatic proof of "denseness" of finset.range (11 messages, latest: Feb 21 2023 at 02:57)
• noetherian top. space (5 messages, latest: Feb 20 2023 at 23:32)
• Direct Sum of Representations (10 messages, latest: Feb 20 2023 at 17:57)
• coercion from nnrat to nnreal? (28 messages, latest: Feb 19 2023 at 16:42)
• iterated mfderiv (6 messages, latest: Feb 18 2023 at 10:41)
• simple_graph.subgraph has Sups and Infs (19 messages, latest: Feb 17 2023 at 17:44)
• ✔ mathematical programming (8 messages, latest: Feb 16 2023 at 22:48)
• ✔ x < y implies x/2 < y/2 (14 messages, latest: Feb 16 2023 at 21:51)
• Number of k-dim subspaces (10 messages, latest: Feb 16 2023 at 19:20)
• pow_zero and pow_succ for integers (2 messages, latest: Feb 16 2023 at 05:28)
• p-adic Valuation of negative numbers (19 messages, latest: Feb 15 2023 at 21:37)
• AD determinacy axiom (3 messages, latest: Feb 14 2023 at 20:21)
• union distributes over nonempty bUnion (3 messages, latest: Feb 14 2023 at 13:57)
• IEEE floats (11 messages, latest: Feb 14 2023 at 11:33)
• a / b / a = b⁻¹ (2 messages, latest: Feb 10 2023 at 14:07)
• Performing computations when applying a lemma (47 messages, latest: Feb 08 2023 at 08:54)
• Casting LCM (8 messages, latest: Feb 08 2023 at 04:03)
• Basic properties of polynomials (24 messages, latest: Feb 07 2023 at 16:49)
• Nilpotent/zero divisors in polynomial/power series ring (13 messages, latest: Feb 06 2023 at 18:32)
• Product of Haar measures (25 messages, latest: Feb 06 2023 at 15:54)
• Discrete valuations (4 messages, latest: Feb 05 2023 at 03:03)
• strongly_measurable.is_lub (10 messages, latest: Feb 03 2023 at 23:09)
• matrices = linear maps (22 messages, latest: Feb 03 2023 at 20:00)
• Partition numbers (12 messages, latest: Feb 03 2023 at 19:03)
• coe summable (7 messages, latest: Feb 03 2023 at 17:54)
• ✔ function that maps a proposition (u ∈ X) to a value (11 messages, latest: Feb 02 2023 at 12:21)
• division and remainder as an equivalence (10 messages, latest: Feb 02 2023 at 11:45)
• ✔ Equality of sets (7 messages, latest: Feb 01 2023 at 22:11)
• ✔ Distribution of Implication (4 messages, latest: Feb 01 2023 at 08:20)
• Ring of integers is a free ℤ-module (17 messages, latest: Jan 31 2023 at 14:38)
• ✔ pigeonhole (16 messages, latest: Jan 29 2023 at 22:33)
• int.cast for fin (5 messages, latest: Jan 27 2023 at 15:08)
• Topology on infinite sequence spaces (10 messages, latest: Jan 27 2023 at 14:21)
• ordinals and induction (55 messages, latest: Jan 27 2023 at 14:14)
• Convex implies monotone secants (15 messages, latest: Jan 25 2023 at 21:42)
• Euclidean Geometry (112 messages, latest: Jan 24 2023 at 00:45)
• ✔ Icc_ge_subsingleton (13 messages, latest: Jan 23 2023 at 08:34)
• X^d - 1 | X^(nd) - 1 (17 messages, latest: Jan 22 2023 at 03:20)
• sensible constructor for add_comm_group (17 messages, latest: Jan 20 2023 at 21:40)
• premeasures (1 message, latest: Jan 20 2023 at 16:04)
• zero module (9 messages, latest: Jan 19 2023 at 22:48)
• coefft of X^j in prod_i (X + a_i) (8 messages, latest: Jan 19 2023 at 22:44)
• existence of equiv mapping nodup same length lists (17 messages, latest: Jan 19 2023 at 08:30)
• Adjoin_root f is a domain for prime f (5 messages, latest: Jan 18 2023 at 23:11)
• make an argument implicit (5 messages, latest: Jan 18 2023 at 22:37)
• Maximum Term Method Help (7 messages, latest: Jan 16 2023 at 21:58)
• Biratio (9 messages, latest: Jan 16 2023 at 20:18)
• Do mathlib have at_top_bot filter (3 messages, latest: Jan 15 2023 at 11:43)
• Affine space over vector span (2 messages, latest: Jan 14 2023 at 13:44)
• 𝔽₄ (17 messages, latest: Jan 12 2023 at 23:08)
• Abel's summation and/or Stieltjes integration (5 messages, latest: Jan 12 2023 at 11:52)
• Equality of ideals from local equality (4 messages, latest: Jan 12 2023 at 11:13)
• Geometry Of Numbers (16 messages, latest: Jan 12 2023 at 05:09)
• ✔ real affine maps (10 messages, latest: Jan 11 2023 at 14:50)
• real affine maps (2 messages, latest: Jan 11 2023 at 14:00)
• Ramsey Theory/Graphs (5 messages, latest: Jan 10 2023 at 18:22)
• Descartes Rule of Signs (31 messages, latest: Jan 09 2023 at 16:34)
• Notation precedence (1 message, latest: Jan 09 2023 at 16:25)
• Alexander's theorem (8 messages, latest: Jan 09 2023 at 05:26)
• Example Code of Matrix Rank (16 messages, latest: Jan 06 2023 at 11:28)
• Enlarge the codomain of a function (5 messages, latest: Jan 05 2023 at 23:13)
• Binomial theorem (28 messages, latest: Jan 05 2023 at 22:20)
• Lattices (the other kind) (4 messages, latest: Jan 05 2023 at 08:49)
• Dirichlet inverses (4 messages, latest: Jan 05 2023 at 00:45)
• ✔ Two ways to sum finsets (14 messages, latest: Jan 04 2023 at 22:25)
• Ostrowski's theorem (21 messages, latest: Jan 04 2023 at 21:41)
• ✔ Set Systems? (29 messages, latest: Jan 04 2023 at 14:11)
• Restricted well-foundedness of docs#prod.lex (4 messages, latest: Jan 04 2023 at 08:33)
• abv a - abv b ≤ abv (a + b) (10 messages, latest: Jan 04 2023 at 00:21)
• ✔ ennreal.mul_div_mul_left (15 messages, latest: Jan 03 2023 at 16:07)
• ennreal.mul_div_mul_left (3 messages, latest: Jan 03 2023 at 15:00)
• Subgroups of zmod (11 messages, latest: Jan 03 2023 at 09:40)
• Reassociating docs#mul_opposite.op (8 messages, latest: Jan 02 2023 at 11:41)
• forget some declaration (7 messages, latest: Jan 02 2023 at 09:36)
• ✔ case splitting in linear order? (13 messages, latest: Jan 01 2023 at 17:20)
• case splitting in linear order? (3 messages, latest: Jan 01 2023 at 16:39)
• [Hyperoperation and 2+2=22=2^2=…](topic/Hyperoperation.20and.202.2B2.3D22.3D2.5E2.3D.2E.2E.2E.html) (4 messages, latest: Jan 01 2023 at 03:28)
• Universal Algebra (13 messages, latest: Dec 30 2022 at 15:43)
• Power basis of adjoin R x (24 messages, latest: Dec 29 2022 at 18:00)
• ✔ finset on linear order to list? (3 messages, latest: Dec 29 2022 at 13:33)
• finset on linear order to list? (1 message, latest: Dec 29 2022 at 12:39)
• le.to_submodule (3 messages, latest: Dec 28 2022 at 19:51)
• ✔ Tactic similar to apply but generates equalities (2 messages, latest: Dec 27 2022 at 18:16)
• Tactic similar to apply but generates equalities (4 messages, latest: Dec 27 2022 at 17:53)
• ✔ does lean have assert? (2 messages, latest: Dec 25 2022 at 02:00)
• Continuity from filters (25 messages, latest: Dec 24 2022 at 15:30)
• does lean have assert? (4 messages, latest: Dec 24 2022 at 14:28)
• divisibilty of powers (38 messages, latest: Dec 24 2022 at 12:49)
• Set is finite if image and fibers are finite? (7 messages, latest: Dec 24 2022 at 11:34)
• ✔ list.take_while_coe? (1 message, latest: Dec 21 2022 at 10:57)
• Set Systems? (18 messages, latest: Dec 21 2022 at 09:49)
• list.take_while_coe? (44 messages, latest: Dec 21 2022 at 09:29)
• ✔ a ≤ a + b in ennreals (29 messages, latest: Dec 21 2022 at 07:30)
• Primes > 2 are odd (16 messages, latest: Dec 20 2022 at 22:51)
• Conjugate elements in same Galois orbit (18 messages, latest: Dec 19 2022 at 18:11)
• Taking element from non-empty set (9 messages, latest: Dec 19 2022 at 14:38)
• logic.relation.symm_gen equivalent (5 messages, latest: Dec 17 2022 at 21:27)
• ✔ is_open {a} from finite balls (3 messages, latest: Dec 17 2022 at 16:20)
• is_open {a} from finite balls (7 messages, latest: Dec 17 2022 at 15:54)
• Tactic to "name" a goal and use it afterwards (6 messages, latest: Dec 17 2022 at 14:44)
• access raw proof terms (6 messages, latest: Dec 17 2022 at 01:01)
• Permutation to make a function monotone (12 messages, latest: Dec 16 2022 at 17:48)
• ✔ Cofinite maps? (25 messages, latest: Dec 16 2022 at 17:29)
• ✔ setup option for simplifier trace_lemmas (8 messages, latest: Dec 15 2022 at 11:33)
• The set of finite sets is well-founded? (23 messages, latest: Dec 14 2022 at 21:03)
• ✔ finset to list (4 messages, latest: Dec 14 2022 at 05:36)
• "backwards" induction on fin (3 messages, latest: Dec 13 2022 at 02:52)
• Isolated point (2 messages, latest: Dec 11 2022 at 14:23)
• If a + b ≤ 2 * c then one of them is ≤ c (33 messages, latest: Dec 11 2022 at 12:04)
• ✔ if list option has none then none (5 messages, latest: Dec 11 2022 at 07:01)
• Identifying endpoints of [0, 1] (17 messages, latest: Dec 10 2022 at 12:24)
• equiv from countable (6 messages, latest: Dec 10 2022 at 09:27)
• forgetting hypothesis definition (3 messages, latest: Dec 10 2022 at 07:29)
• Structures vs Type classes: Projections (8 messages, latest: Dec 08 2022 at 17:44)
• More general version of list.map_const? (8 messages, latest: Dec 08 2022 at 15:47)
• Trichotomy of int.sign (15 messages, latest: Dec 06 2022 at 03:31)
• ✔ Showing 2 * int is not equal to 3 (6 messages, latest: Dec 05 2022 at 20:52)
• ✔ Represent a ideal generated by an integer (3 messages, latest: Dec 05 2022 at 17:31)
• Represent a ideal generated by an integer (36 messages, latest: Dec 05 2022 at 12:29)
• Euclid's division lemma (6 messages, latest: Dec 01 2022 at 20:47)
• pi.monoid_hom (4 messages, latest: Nov 29 2022 at 20:46)
• ✔ Declaring rings and ideals, and proving ideal is subset (10 messages, latest: Nov 29 2022 at 17:51)
• minimal polynomial of inverse (3 messages, latest: Nov 29 2022 at 16:02)
• Baire Category Stuff (1 message, latest: Nov 29 2022 at 12:59)
• Totient decidability (18 messages, latest: Nov 27 2022 at 18:45)
• ✔ Is there a mul_left_inj for rings..? (3 messages, latest: Nov 26 2022 at 22:53)
• Is there a mul_left_inj for rings..? (9 messages, latest: Nov 26 2022 at 18:38)
• ✔ x ≤ y \ z from disjoint x z and x ≤ y (2 messages, latest: Nov 26 2022 at 08:22)
• x ≤ y \ z from disjoint x z and x ≤ y (3 messages, latest: Nov 26 2022 at 07:44)
• multivariate chain rule for polynomials (4 messages, latest: Nov 23 2022 at 20:35)
• ✔ Rewrite once (1 message, latest: Nov 23 2022 at 14:33)
• Rewrite once (15 messages, latest: Nov 23 2022 at 13:16)
• kTop is CCC (21 messages, latest: Nov 23 2022 at 00:32)
• Exporting all the proof terms (4 messages, latest: Nov 22 2022 at 15:25)
• ✔ instance has_mul for structure (6 messages, latest: Nov 21 2022 at 20:47)
• ✔ Is there a instance of "ring with (mul) inverse" (6 messages, latest: Nov 21 2022 at 16:49)
• fin.next (9 messages, latest: Nov 21 2022 at 07:46)
• Support functional (5 messages, latest: Nov 20 2022 at 09:48)
• coe_is_monoid_hom transitivity (9 messages, latest: Nov 19 2022 at 18:15)
• from rationals to reals (4 messages, latest: Nov 18 2022 at 22:49)
• Defining functions for structures (29 messages, latest: Nov 18 2022 at 17:44)
• "exactly one of the following is true" (11 messages, latest: Nov 18 2022 at 14:38)
• Intersection of localisations (26 messages, latest: Nov 18 2022 at 04:05)
• Weights on polynomial rings, etc (4 messages, latest: Nov 17 2022 at 10:35)
• Reasoning about Algorithms (6 messages, latest: Nov 16 2022 at 23:00)
• Products of iterated derivatives (2 messages, latest: Nov 16 2022 at 14:37)
• pushforward/pullback of sheaves (14 messages, latest: Nov 16 2022 at 13:39)
• ✔ lift a theorem on a type to a subtype? (5 messages, latest: Nov 15 2022 at 13:47)
• lift a theorem on a type to a subtype? (6 messages, latest: Nov 15 2022 at 13:08)
• ✔ Mul eq implies a ne 0 (for div_ring) (4 messages, latest: Nov 15 2022 at 11:14)
• Mul eq implies a ne 0 (for div_ring) (3 messages, latest: Nov 15 2022 at 11:01)
• Obtain isomorphism from short exact sequence (40 messages, latest: Nov 14 2022 at 21:40)
• Is there a mul_lt_iff_lt_div (9 messages, latest: Nov 13 2022 at 17:28)
• ✔ Is there a way to remove a hypothesis (4 messages, latest: Nov 12 2022 at 16:02)
• ✔ Subtraction cancellation in a lt (4 messages, latest: Nov 12 2022 at 15:21)
• Subtraction cancellation in a lt (1 message, latest: Nov 12 2022 at 15:00)
• Product of integers is -1 [title changed] (6 messages, latest: Nov 12 2022 at 13:48)
• bottom type (⊥) (13 messages, latest: Nov 12 2022 at 03:22)
• eq_neg_iff_neg_eq? (23 messages, latest: Nov 11 2022 at 22:14)
• no_confusion_heq tactic? (21 messages, latest: Nov 11 2022 at 16:59)
• non_assoc_ring is not a monoid_with_zero? (32 messages, latest: Nov 11 2022 at 09:06)
• Composition of algebras (5 messages, latest: Nov 11 2022 at 07:56)
• is_subgroup H G (10 messages, latest: Nov 10 2022 at 19:55)
• ✔ sum.map f g is bijective if both f and g are. (6 messages, latest: Nov 10 2022 at 17:39)
• sum.map f g is bijective if both f and g are. (3 messages, latest: Nov 10 2022 at 17:04)
• Artinian/noetherian lattice (4 messages, latest: Nov 09 2022 at 13:55)
• semiring and cancel_comm_monoid_with_zero (37 messages, latest: Nov 08 2022 at 18:40)
• linear combination is in span (12 messages, latest: Nov 08 2022 at 00:31)
• list end-appending (4 messages, latest: Nov 07 2022 at 18:13)
• Instance management (8 messages, latest: Nov 07 2022 at 08:33)
• list.nodup iff length equal cardinality (8 messages, latest: Nov 06 2022 at 13:06)
• Small enough balls (11 messages, latest: Nov 05 2022 at 22:41)
• dirichlet character (4 messages, latest: Nov 03 2022 at 15:16)
• [specialize h , swap](topic/specialize.20h.20.2C.20swap.html) (10 messages, latest: Nov 03 2022 at 02:22)
• ae finite function of convergent integral (8 messages, latest: Nov 02 2022 at 19:03)
• re-casting to nat (11 messages, latest: Nov 01 2022 at 17:03)
• ✔ list.join.take (1 message, latest: Nov 01 2022 at 16:36)
• folklore/"joke" theorem (8 messages, latest: Oct 31 2022 at 21:38)
• Contraposition Equivalence in Lean4 somewhere? (1 message, latest: Oct 28 2022 at 23:02)
• Operations on uniform limits (47 messages, latest: Oct 28 2022 at 17:10)
• Splitting a finite list as sublists (4 messages, latest: Oct 28 2022 at 13:54)
• Algebra trace equals sum of roots of charpoly (7 messages, latest: Oct 28 2022 at 12:04)
• 1 ≠ -1 in ℤˣ? (22 messages, latest: Oct 27 2022 at 20:08)
• measurable_space ℤˣ (3 messages, latest: Oct 26 2022 at 21:18)
• Preimage of defined subset of \R (8 messages, latest: Oct 26 2022 at 21:11)
• Finsupp generalisations (21 messages, latest: Oct 26 2022 at 19:03)
• ✔ Left coset notation (26 messages, latest: Oct 26 2022 at 09:07)
• list.join.take (27 messages, latest: Oct 26 2022 at 09:00)
• Does Lean4 provide contraposition in somewhere? (1 message, latest: Oct 26 2022 at 02:12)
• ✔ Is there a tactic to expand a forall (1 message, latest: Oct 25 2022 at 19:28)
• (p, q).snd (13 messages, latest: Oct 24 2022 at 20:43)
• Convention for the order on topologies (7 messages, latest: Oct 24 2022 at 19:10)
• Is there a tactic to expand a forall (3 messages, latest: Oct 24 2022 at 15:21)
• ✔ "Big intersection" of sets (6 messages, latest: Oct 24 2022 at 15:13)
• Characterisation of connectedness using continuous maps (59 messages, latest: Oct 24 2022 at 14:47)
• ✔ dense_inducing extension of uniform_continuous functions (2 messages, latest: Oct 24 2022 at 13:46)
• dense_inducing extension of uniform_continuous functions (12 messages, latest: Oct 24 2022 at 07:23)
• ✔ eps-N rule for real (4 messages, latest: Oct 23 2022 at 20:50)
• Proper maps (in the sense of topology) (18 messages, latest: Oct 22 2022 at 15:31)
• Empty function (4 messages, latest: Oct 22 2022 at 15:23)
• ✔ Unfolding the definition of a member of a smul (2 messages, latest: Oct 21 2022 at 20:01)
• Unfolding the definition of a member of a smul (7 messages, latest: Oct 21 2022 at 10:22)
• Open set of reals contains ball/interval (25 messages, latest: Oct 21 2022 at 07:54)
• Product of subgroups (5 messages, latest: Oct 21 2022 at 04:42)
• ✔ Pull predicate from has_mem expr (6 messages, latest: Oct 20 2022 at 20:35)
• Pull predicate from has_mem expr (3 messages, latest: Oct 20 2022 at 20:16)
• ✔ Finite types (1 message, latest: Oct 20 2022 at 19:30)
• ✔ withType (4 messages, latest: Oct 20 2022 at 02:43)
• Complex roots of unity as a finset (18 messages, latest: Oct 20 2022 at 01:34)
• Ergodic maps / measures (5 messages, latest: Oct 18 2022 at 12:29)
• ✔ Mapping injective function (3 messages, latest: Oct 18 2022 at 12:13)
• Locally uniform convergence (9 messages, latest: Oct 18 2022 at 00:00)
• sum over bigger finset (4 messages, latest: Oct 17 2022 at 23:21)
• Attribute Domains (4 messages, latest: Oct 17 2022 at 16:30)
• Check which imported definitions are used (4 messages, latest: Oct 17 2022 at 07:43)
• finsupp equals sum of finsupp.filter (2 messages, latest: Oct 15 2022 at 19:23)
• Int version of caseswork of divisors (4 messages, latest: Oct 15 2022 at 17:08)
• Casts as actions (11 messages, latest: Oct 15 2022 at 16:00)
• kernel of a semiring action (17 messages, latest: Oct 15 2022 at 14:41)
• group with two elements (14 messages, latest: Oct 14 2022 at 01:49)
• Group (/monoid) rings (7 messages, latest: Oct 13 2022 at 11:43)
• How many elements of order two does S_4 have (7 messages, latest: Oct 12 2022 at 22:01)
• smooth vector field on manifold (1 message, latest: Oct 12 2022 at 21:46)
• free product of 2 groups (8 messages, latest: Oct 12 2022 at 21:15)
• mul_one_class, group… instances for dependend pi (5 messages, latest: Oct 12 2022 at 11:22)
• Equalities which are “the wrong way round” involving boun… (9 messages, latest: Oct 11 2022 at 23:09)
• tsum_ite_eq_extract for monoid (5 messages, latest: Oct 11 2022 at 19:13)
• to_prefunctor_ext ? (8 messages, latest: Oct 11 2022 at 16:49)
• Computation of an explicit sum (11 messages, latest: Oct 11 2022 at 15:07)
• Accumulation point (61 messages, latest: Oct 10 2022 at 08:50)
• Module localization (10 messages, latest: Oct 10 2022 at 08:32)
• forgetting a hypothesis (2 messages, latest: Oct 08 2022 at 00:24)
• Extending well-founded relation to well-order (17 messages, latest: Oct 07 2022 at 23:05)
• coe from finset.subtype to finset (16 messages, latest: Oct 07 2022 at 04:15)
• golf nat.coprime proof (20 messages, latest: Oct 06 2022 at 22:52)
• Term representing match (10 messages, latest: Oct 06 2022 at 20:43)
• matrix.eq_zero_of_mul_eq_zero (4 messages, latest: Oct 06 2022 at 17:12)
• supremum of pointwise product of sets of real numbers (4 messages, latest: Oct 06 2022 at 14:09)
• ✔ ∀ (m : ℤ), - m * 2 ≠ 1 (6 messages, latest: Oct 05 2022 at 15:55)
• Vector of ones (3 messages, latest: Oct 05 2022 at 02:46)
• namespace in metaprogramming (5 messages, latest: Oct 05 2022 at 02:01)
• congruence of filters for tendsto (110 messages, latest: Oct 04 2022 at 18:37)
• continuity of derivative in a different argument (2 messages, latest: Oct 04 2022 at 05:54)
• Ioo (a ⊓ b) a ≃o Ioo b (a ⊔ b) (2 messages, latest: Oct 03 2022 at 08:46)
• "sort" a function (79 messages, latest: Oct 03 2022 at 02:16)
• Hyperplane is closed or dense (3 messages, latest: Oct 02 2022 at 20:56)
• Lebesgue Density Theorem (7 messages, latest: Oct 02 2022 at 15:16)
• Uniform separation of compact and closed set (5 messages, latest: Oct 01 2022 at 20:04)
• Kaminski's Equation (67 messages, latest: Sep 30 2022 at 16:06)
• Finite state machines / transducers (5 messages, latest: Sep 30 2022 at 13:03)
• Simple ring lemma (42 messages, latest: Sep 29 2022 at 23:09)
• Help proving well_foundedness (13 messages, latest: Sep 28 2022 at 20:16)
• How to make a Blueprint (59 messages, latest: Sep 28 2022 at 16:34)
• Finite basis with small vectors (2 messages, latest: Sep 28 2022 at 08:35)
• name function without function body (5 messages, latest: Sep 28 2022 at 03:13)
• continuous on an open set (9 messages, latest: Sep 27 2022 at 22:07)
• Eliminate part of a product type from tsum (5 messages, latest: Sep 27 2022 at 16:23)
• polynomial ext with degree bound (42 messages, latest: Sep 27 2022 at 14:38)
• galois insertion (co)atoms (2 messages, latest: Sep 26 2022 at 14:24)
• least element principle (8 messages, latest: Sep 25 2022 at 22:16)
• ✔ Constant functions are analytic (2 messages, latest: Sep 25 2022 at 15:52)
• int.mod_by_nat (20 messages, latest: Sep 24 2022 at 00:16)
• Completion of a complete space (23 messages, latest: Sep 23 2022 at 19:40)
• exponential function to a natural power (4 messages, latest: Sep 23 2022 at 07:00)
• Subspace Topology (32 messages, latest: Sep 22 2022 at 23:53)
• composing functions (4 messages, latest: Sep 22 2022 at 22:14)
• Maximal independent set of a graph (3 messages, latest: Sep 22 2022 at 13:11)
• adding angles (80 messages, latest: Sep 22 2022 at 07:26)
• ✔ List containing unique natural numbers (23 messages, latest: Sep 22 2022 at 07:22)
• fin zip (13 messages, latest: Sep 22 2022 at 05:09)
• Formal Series (5 messages, latest: Sep 22 2022 at 01:14)
• ✔ Morphisms of quivers (3 messages, latest: Sep 21 2022 at 09:52)
• more picard_lindelof (14 messages, latest: Sep 21 2022 at 03:09)
• ideal.nat_cast (22 messages, latest: Sep 20 2022 at 12:23)
• Cauchy sequences are totally bounded (4 messages, latest: Sep 20 2022 at 05:13)
• finset from a finite subset of an infinite set (23 messages, latest: Sep 17 2022 at 13:06)
• Constant functions are analytic (6 messages, latest: Sep 16 2022 at 17:28)
• Formal verification of LLVM? (14 messages, latest: Sep 15 2022 at 13:17)
• real complex smul_comm_class (13 messages, latest: Sep 14 2022 at 23:50)
• Order on fin n.succ (21 messages, latest: Sep 14 2022 at 10:51)
• or.elim_left/right (9 messages, latest: Sep 14 2022 at 10:38)
• Nested intervals (4 messages, latest: Sep 14 2022 at 03:59)
• 1/2 is not an integer (18 messages, latest: Sep 13 2022 at 22:32)
• ✔ Taylor series (2 messages, latest: Sep 13 2022 at 16:03)
• Prop as canonically_ordered_monoid (12 messages, latest: Sep 13 2022 at 15:47)
• is_open_set_of_eventually_nhds_within (5 messages, latest: Sep 13 2022 at 13:10)
• Integrability of powers of norm (16 messages, latest: Sep 13 2022 at 05:44)
• Sum over characteristic function (40 messages, latest: Sep 12 2022 at 23:10)
• fin.range (2 messages, latest: Sep 12 2022 at 17:15)
• Taylor series (7 messages, latest: Sep 12 2022 at 13:49)
• canonically_linear_ordered_monoid.to_linear_ordered_comm_… (1 message, latest: Sep 11 2022 at 21:24)
• ✔ converse of nat.sub_le_sub_left (13 messages, latest: Sep 11 2022 at 18:08)
• Finite cyclic graphs (7 messages, latest: Sep 11 2022 at 17:39)
• Lists (5 messages, latest: Sep 09 2022 at 23:38)
• Pseudometric def of uniform space (26 messages, latest: Sep 08 2022 at 21:00)
• ✔ Product of locally finite simple graphs (15 messages, latest: Sep 08 2022 at 14:22)
• canonically_ordered_monoid not inhabited? (8 messages, latest: Sep 08 2022 at 13:09)
• ✔ Binomial coefficients (2 messages, latest: Sep 08 2022 at 08:28)
• Binomial coefficients (3 messages, latest: Sep 08 2022 at 08:08)
• Product of locally finite simple graphs (5 messages, latest: Sep 08 2022 at 07:37)
• bit0/bit1 and mod (9 messages, latest: Sep 06 2022 at 10:31)
• Properties of products (56 messages, latest: Sep 02 2022 at 17:51)
• injective + mul bundling (4 messages, latest: Sep 01 2022 at 20:52)
• Monoidal functor from preserves limits/colimits (1 message, latest: Sep 01 2022 at 17:39)
• unique products (65 messages, latest: Sep 01 2022 at 12:19)
• .inj (6 messages, latest: Sep 01 2022 at 07:47)
• Constraints on lambda function (22 messages, latest: Aug 31 2022 at 21:48)
• Can't infer nontrivial ℝ (16 messages, latest: Aug 31 2022 at 19:05)
• Largest element satisfying P in range (4 messages, latest: Aug 31 2022 at 16:10)
• normed structures on quotients (20 messages, latest: Aug 31 2022 at 13:32)
• is_regular.inj (22 messages, latest: Aug 30 2022 at 19:43)
• Continuity and inducing (4 messages, latest: Aug 30 2022 at 07:28)
• Sorting is injective (6 messages, latest: Aug 30 2022 at 07:07)
• A tactic for "reaching" inside a quantified statement? (5 messages, latest: Aug 29 2022 at 23:47)
• ext for linear maps from a tensor product (7 messages, latest: Aug 28 2022 at 21:20)
• order of one in zmod (13 messages, latest: Aug 28 2022 at 06:32)
• cardinal.le_of_add_le_add (14 messages, latest: Aug 26 2022 at 15:18)
• Fin k -> Fin (k + n) (2 messages, latest: Aug 26 2022 at 10:13)
• Moore-Smith sequences (7 messages, latest: Aug 25 2022 at 17:23)
• restricted set of equality points is closed (10 messages, latest: Aug 24 2022 at 14:56)
• computable finset to list (3 messages, latest: Aug 24 2022 at 05:21)
• Composing finite number of morphisms? (5 messages, latest: Aug 24 2022 at 03:20)
• Subfunctors (16 messages, latest: Aug 23 2022 at 16:40)
• Decomposition of the symmetry group of euclidean space (3 messages, latest: Aug 23 2022 at 06:12)
• Factoring zero roots (20 messages, latest: Aug 22 2022 at 08:57)
• supr₂_add (5 messages, latest: Aug 21 2022 at 23:23)
• ✔ Prop structure equivalent to its components? (8 messages, latest: Aug 21 2022 at 22:51)
• open interval (14 messages, latest: Aug 21 2022 at 11:20)
• ✔ integrability under translation (2 messages, latest: Aug 21 2022 at 09:51)
• integrability under translation (4 messages, latest: Aug 21 2022 at 05:57)
• model finding (11 messages, latest: Aug 19 2022 at 20:23)
• Real as limit of sequence of rationals (38 messages, latest: Aug 19 2022 at 00:00)
• Discrete subgroup of Hausdorff group is closed (18 messages, latest: Aug 18 2022 at 14:56)
• ne_zero without mul_zero_class (3 messages, latest: Aug 18 2022 at 14:17)
• ✔ forall₂ nth_le (2 messages, latest: Aug 17 2022 at 23:01)
• smul_mem_class (2 messages, latest: Aug 17 2022 at 21:54)
• ✔ set α in fintype α (5 messages, latest: Aug 17 2022 at 14:57)
• nat.exists_eq_supr (5 messages, latest: Aug 17 2022 at 08:23)
• universal morphism in category theory (2 messages, latest: Aug 17 2022 at 04:36)
• pointwise ops on nhds (6 messages, latest: Aug 16 2022 at 17:22)
• opening the square (14 messages, latest: Aug 16 2022 at 17:11)
• check all the cases mod 4 (5 messages, latest: Aug 16 2022 at 13:31)
• forall₂ nth_le (25 messages, latest: Aug 16 2022 at 13:25)
• ✔ limit of a nonnegative sequence is nonnegative (4 messages, latest: Aug 16 2022 at 04:25)
• ✔ natural transformation horizontal composition (1 message, latest: Aug 14 2022 at 17:52)
• natural transformation horizontal composition (3 messages, latest: Aug 14 2022 at 15:23)
• Continuous complex ring hom (17 messages, latest: Aug 14 2022 at 12:32)
• continuity of continuous composition (44 messages, latest: Aug 12 2022 at 12:32)
• is_open_bInter_finset (14 messages, latest: Aug 12 2022 at 12:18)
• checking a proof uses all its assumptions (38 messages, latest: Aug 12 2022 at 08:33)
• list.sorted with list.map? (2 messages, latest: Aug 12 2022 at 06:30)
• f x = 1 for subsingletons (2 messages, latest: Aug 11 2022 at 17:03)
• countably infinite type ≃ ℕ (4 messages, latest: Aug 11 2022 at 07:29)
• ✔ ∀ (x : ℝ), is_algebraic ℚ x ↔ is_algebraic ℤ x (3 messages, latest: Aug 11 2022 at 03:05)
• filtering a (finite) group to a subgroup (12 messages, latest: Aug 11 2022 at 01:01)
• ✔ sub one succ (1 message, latest: Aug 10 2022 at 23:13)
• sub one succ (2 messages, latest: Aug 10 2022 at 23:13)
• Multinomial theorem (3 messages, latest: Aug 10 2022 at 20:55)
• linear order on finsupps (35 messages, latest: Aug 10 2022 at 18:29)
• ennreal.supr_coe (12 messages, latest: Aug 10 2022 at 14:42)
• more linear algebra (5 messages, latest: Aug 10 2022 at 14:34)
• How to prove well-founded recursion (3 messages, latest: Aug 10 2022 at 01:13)
• Banach–Alaoglu theorem (37 messages, latest: Aug 09 2022 at 19:55)
• metric bounded for normed space (4 messages, latest: Aug 09 2022 at 15:51)
• module.free ℝ (fin 2 → ℝ) (10 messages, latest: Aug 09 2022 at 13:02)
• ∀ (x : ℝ), is_algebraic ℚ x ↔ is_algebraic ℤ x (2 messages, latest: Aug 09 2022 at 09:34)
• some linear algebra (28 messages, latest: Aug 09 2022 at 05:54)
• squares equal iff args are (19 messages, latest: Aug 08 2022 at 23:50)
• ✔ Repeated Function Composition (2 messages, latest: Aug 08 2022 at 23:34)
• Repeated Function Composition (4 messages, latest: Aug 08 2022 at 22:36)
• ✔ a % (b * c) % c = a % c (1 message, latest: Aug 08 2022 at 17:41)
• fdifferential to tangent_space (2 messages, latest: Aug 08 2022 at 08:01)
• a % (b * c) % c = a % c (3 messages, latest: Aug 07 2022 at 20:38)
• Trivial ite lemma (19 messages, latest: Aug 07 2022 at 17:21)
• the "augmentation ideal" of a multivariable polynomial ring (5 messages, latest: Aug 06 2022 at 23:02)
• is_limit for an object (11 messages, latest: Aug 06 2022 at 15:42)
• matrix groups and Lie groups (43 messages, latest: Aug 05 2022 at 23:15)
• ✔ function equivalence (4 messages, latest: Aug 05 2022 at 12:14)
• continuous_linear_map.eval (9 messages, latest: Aug 05 2022 at 05:14)
• ✔ Ultrafilter convergence theorem? (4 messages, latest: Aug 04 2022 at 14:43)
• Raising absolute values to powers (9 messages, latest: Aug 04 2022 at 05:57)
• ✔ mul_lt_left (5 messages, latest: Aug 04 2022 at 00:58)
• continuity of extension to completion (1 message, latest: Aug 03 2022 at 23:26)
• Restriction of a sum ignoring zeros (6 messages, latest: Aug 03 2022 at 20:17)
• equation in ℕ to equation in zmod n (27 messages, latest: Aug 03 2022 at 19:00)
• ✔ equation in ℕ to equation in zmod n (7 messages, latest: Aug 03 2022 at 14:45)
• ✔ Cardinality for set of a fintype (9 messages, latest: Aug 03 2022 at 07:34)
• ✔ Fubini for finite sums (4 messages, latest: Aug 03 2022 at 03:06)
• exists_monic_map_eq_of_mem_range (12 messages, latest: Aug 02 2022 at 17:55)
• Existence from almost always and non-zero measure (8 messages, latest: Aug 02 2022 at 10:31)
• absolute value and complex conjugate (10 messages, latest: Aug 02 2022 at 02:32)
• ✔ complex.cos θ = real.cos θ (3 messages, latest: Aug 01 2022 at 19:42)
• ✔ splitting field as an intermediate_field (15 messages, latest: Aug 01 2022 at 17:56)
• cos x = 1/2 ↔ … (2 messages, latest: Aug 01 2022 at 00:31)
• ✔ c ∈ set.Icc a b → (d * c) ∈ set.Icc (d * a) (d * b) (3 messages, latest: Jul 31 2022 at 21:54)
• x ∈ {y, z} ↔ (x = y ∨ x = z) (19 messages, latest: Jul 31 2022 at 21:35)
• ✔ Intersection of a chain of nonempty finsets is nonempty. (33 messages, latest: Jul 31 2022 at 21:07)
• c ∈ set.Icc a b → (d * c) ∈ set.Icc (d * a) (d * b) (6 messages, latest: Jul 31 2022 at 20:46)
• ✔ judging for the same constructor (2 messages, latest: Jul 31 2022 at 15:12)
• judging for the same constructor (1 message, latest: Jul 31 2022 at 05:07)
• Niven's theorem (4 messages, latest: Jul 30 2022 at 22:39)
• bundled surjective function (8 messages, latest: Jul 30 2022 at 17:21)
• Intersection of a chain of nonempty finsets is nonempty. (6 messages, latest: Jul 30 2022 at 09:52)
• Elements of completion as limits (23 messages, latest: Jul 30 2022 at 04:28)
• continuity of sums (3 messages, latest: Jul 29 2022 at 16:20)
• Stabilizer of a set (3 messages, latest: Jul 29 2022 at 13:09)
• concrete matrix multiplication (38 messages, latest: Jul 29 2022 at 09:41)
• products over (fin n) (26 messages, latest: Jul 28 2022 at 21:17)
• tendsto equivalent to is bounded (39 messages, latest: Jul 28 2022 at 20:26)
• |x|<epsilon for all epsilon (5 messages, latest: Jul 28 2022 at 16:29)
• Zippers (2 messages, latest: Jul 27 2022 at 21:51)
• Sorting by function value (17 messages, latest: Jul 27 2022 at 17:31)
• ✔ list.nth_le and list.nth (2 messages, latest: Jul 27 2022 at 15:39)
• list.nth_le and list.nth (19 messages, latest: Jul 27 2022 at 13:48)
• ✔ numpy/jax etc? (4 messages, latest: Jul 27 2022 at 02:47)
• explicit sums (34 messages, latest: Jul 25 2022 at 16:14)
• ✔ nat_degree of p + C a (5 messages, latest: Jul 22 2022 at 10:06)
• repr of reals (10 messages, latest: Jul 22 2022 at 03:24)
• non-unital subrings (6 messages, latest: Jul 21 2022 at 17:51)
• Multiplying sparse infinite matricies. (7 messages, latest: Jul 21 2022 at 14:14)
• Point close to the frontier (4 messages, latest: Jul 21 2022 at 09:41)
• Convergent sequences (16 messages, latest: Jul 21 2022 at 01:39)
• Planar geometry with Cartesian coordinates (60 messages, latest: Jul 20 2022 at 21:02)
• list equivalence relation (12 messages, latest: Jul 20 2022 at 20:25)
• submonoid.map_closure (3 messages, latest: Jul 20 2022 at 12:37)
• Induced subgraphs (30 messages, latest: Jul 19 2022 at 18:34)
• exists and forall in subsingleton (5 messages, latest: Jul 19 2022 at 15:08)
• Closest point on a line to a point not on it (18 messages, latest: Jul 19 2022 at 03:31)
• Bifunctor whiskering (23 messages, latest: Jul 19 2022 at 00:47)
• Local minimum of a function from second derivative (6 messages, latest: Jul 18 2022 at 19:54)
• add_tsub_add_le_tsub_add_tsub (9 messages, latest: Jul 18 2022 at 15:53)
• finset.sum eq sum over support (3 messages, latest: Jul 17 2022 at 15:51)
• induction on finite set (10 messages, latest: Jul 17 2022 at 07:53)
• ✔ pairwise (≠) of pairwise (<) (3 messages, latest: Jul 17 2022 at 01:03)
• ✔ is_localization.mk'_pow (2 messages, latest: Jul 15 2022 at 16:38)
• is_localization.mk'_pow (2 messages, latest: Jul 15 2022 at 15:47)
• Filter on (set X) (5 messages, latest: Jul 15 2022 at 07:05)
• Embedding is local (22 messages, latest: Jul 14 2022 at 17:26)
• Initial segment (3 messages, latest: Jul 14 2022 at 16:15)
• sum.lex and prod.lex as rel_embeddings (19 messages, latest: Jul 14 2022 at 16:07)
• to_list_map_prod (34 messages, latest: Jul 14 2022 at 11:51)
• inner product space eq (6 messages, latest: Jul 14 2022 at 06:27)
• downward-closedness under a general relation (24 messages, latest: Jul 14 2022 at 03:40)
• ✔ Image equals image after surjection (3 messages, latest: Jul 13 2022 at 20:54)
• Image equals image after surjection (2 messages, latest: Jul 13 2022 at 18:00)
• cyclic ring (31 messages, latest: Jul 13 2022 at 14:06)
• Equivariant Functions (10 messages, latest: Jul 13 2022 at 12:30)
• tsum stretcher, adding zeroes to sums like this (10 messages, latest: Jul 13 2022 at 08:40)
• with_bot.neg (36 messages, latest: Jul 13 2022 at 05:04)
• lemma exp_pi_mul_I_half : exp (↑real.pi * I / 2) = I := (2 messages, latest: Jul 13 2022 at 02:55)
• Splitting a complex summable tsum into real and imaginary (11 messages, latest: Jul 12 2022 at 22:40)
• tensor product of two A-algebras (6 messages, latest: Jul 12 2022 at 22:32)
• subsingleton (R →ₐ[R] A) (11 messages, latest: Jul 12 2022 at 16:30)
• Scalar multiplication on the right (9 messages, latest: Jul 12 2022 at 13:28)
• Extending intervals (13 messages, latest: Jul 12 2022 at 13:27)
• Sheafification section is amalgamation (8 messages, latest: Jul 12 2022 at 13:15)
• symmetric.on (4 messages, latest: Jul 12 2022 at 13:11)
• limsup_antitone_continuous_eq_antitone_continuous_liminf (11 messages, latest: Jul 11 2022 at 19:37)
• Euler's Formula (4 messages, latest: Jul 10 2022 at 20:48)
• Counting divisible by p (3 messages, latest: Jul 10 2022 at 17:00)
• max_eq_max' (6 messages, latest: Jul 09 2022 at 20:14)
• finsupp from input/output pairs (22 messages, latest: Jul 09 2022 at 15:59)
• Exterior Differential Systems (8 messages, latest: Jul 09 2022 at 12:18)
• Matrix invertible if row lin. independent (2 messages, latest: Jul 09 2022 at 08:44)
• Neighborhoods of sets (13 messages, latest: Jul 08 2022 at 14:17)
• coe and option (22 messages, latest: Jul 08 2022 at 13:18)
• order isomorphism between ℕ and ℕ+ (3 messages, latest: Jul 08 2022 at 08:19)
• has_smul ℚ k for field k (7 messages, latest: Jul 08 2022 at 07:56)
• rel_iso (<) (<) from order_iso (2 messages, latest: Jul 08 2022 at 04:13)
• definition of exp using tsum (13 messages, latest: Jul 08 2022 at 02:56)
• module.prod (18 messages, latest: Jul 07 2022 at 23:53)
• vector space (6 messages, latest: Jul 07 2022 at 21:10)
• Diagonal from a function (3 messages, latest: Jul 07 2022 at 17:49)
• nat.succ as an embedding (14 messages, latest: Jul 07 2022 at 16:34)
• Exponential of reals are real - as a subset of complex (3 messages, latest: Jul 07 2022 at 02:52)
• tactics to prove an equality of reals (3 messages, latest: Jul 05 2022 at 21:04)
• Limit of addition of functions (4 messages, latest: Jul 05 2022 at 16:08)
• Subalgebra to subring (8 messages, latest: Jul 04 2022 at 23:07)
• equivalent to zify for rationals (9 messages, latest: Jul 04 2022 at 05:08)
• pointwise conj_act on normal subgroups (4 messages, latest: Jul 03 2022 at 22:56)
• division algorithm (17 messages, latest: Jul 03 2022 at 18:24)
• Cayley-Hamilton theorem (22 messages, latest: Jul 03 2022 at 12:52)
• Open interval is open (3 messages, latest: Jul 02 2022 at 20:57)
• Sum is in span (14 messages, latest: Jul 02 2022 at 15:48)
• adjoin finset is number field (7 messages, latest: Jul 02 2022 at 06:36)
• canonical isomorphism between localizations (10 messages, latest: Jul 01 2022 at 08:57)
• fin (s.card) finset equiv (76 messages, latest: Jul 01 2022 at 07:26)
• induced/coinduced topology for a family of maps (3 messages, latest: Jun 30 2022 at 22:13)
• Coding theory and code-based crypography (72 messages, latest: Jun 30 2022 at 14:22)
• coercion from Z to R (2 messages, latest: Jun 30 2022 at 05:14)
• Two induction principles (9 messages, latest: Jun 29 2022 at 21:29)
• Scalar multiplication on functions (7 messages, latest: Jun 28 2022 at 16:40)
• dite (h : P ∧ Q) and split_ifs (4 messages, latest: Jun 28 2022 at 15:11)
• Hyperbolic Geometry (12 messages, latest: Jun 28 2022 at 11:58)
• additive of subgroup (3 messages, latest: Jun 28 2022 at 11:05)
• ✔ function with singleton support (5 messages, latest: Jun 28 2022 at 00:50)
• Graph Theory (159 messages, latest: Jun 27 2022 at 19:25)
• exists iff exists (4 messages, latest: Jun 27 2022 at 15:20)
• ✔ field_simp for units (7 messages, latest: Jun 27 2022 at 13:16)
• Finite chain has a maximal element (6 messages, latest: Jun 27 2022 at 12:58)
• determinant via exterior algebra (117 messages, latest: Jun 26 2022 at 21:31)
• Decidability of is_unit on finite rings (35 messages, latest: Jun 26 2022 at 20:15)
• Length of longest chain (9 messages, latest: Jun 26 2022 at 16:20)
• Lie bracket, algebraic version (3 messages, latest: Jun 26 2022 at 03:07)
• Sesquilinear form (6 messages, latest: Jun 25 2022 at 23:41)
• field_simp for units (39 messages, latest: Jun 24 2022 at 15:25)
• is_empty ↥s (3 messages, latest: Jun 24 2022 at 05:36)
• Arithmetic function and general functions (12 messages, latest: Jun 23 2022 at 17:41)
• List of expressions to expression for that list (8 messages, latest: Jun 22 2022 at 20:48)
• Infinite product (8 messages, latest: Jun 22 2022 at 19:16)
• ✔ equivalence between multiple well-founded relation defi… (4 messages, latest: Jun 22 2022 at 17:16)
• ✔ subgraphs (2 messages, latest: Jun 22 2022 at 08:56)
• "Projecting" a sigma type (4 messages, latest: Jun 22 2022 at 08:41)
• multiplicity of root in extension field (14 messages, latest: Jun 22 2022 at 05:52)
• subgraphs (18 messages, latest: Jun 21 2022 at 17:01)
• ✔ multiset.prod = list.prod (4 messages, latest: Jun 21 2022 at 16:35)
• Convex hull membership (4 messages, latest: Jun 20 2022 at 16:06)
• ✔ map (succ : ℕ → ℕ) at_top = at_top (6 messages, latest: Jun 20 2022 at 12:04)
• Uniform discreteness and relative density (1 message, latest: Jun 20 2022 at 11:03)
• Set is a submodule (3 messages, latest: Jun 20 2022 at 10:36)
• finset α ≃ set α (17 messages, latest: Jun 20 2022 at 07:56)
• powers of an endofunctor (1 message, latest: Jun 20 2022 at 06:52)
• Composition of convex functions (2 messages, latest: Jun 19 2022 at 22:50)
• rat.cast_sum (7 messages, latest: Jun 19 2022 at 16:44)
• bijection (7 messages, latest: Jun 19 2022 at 02:22)
• Gcd of a set of natural numbers or integers (4 messages, latest: Jun 17 2022 at 19:37)
• Pullback well-foundedness (3 messages, latest: Jun 17 2022 at 17:13)
• ✔ Specific integrals (2 messages, latest: Jun 17 2022 at 07:14)
• Specific integrals (1 message, latest: Jun 17 2022 at 07:13)
• Fixed point (6 messages, latest: Jun 16 2022 at 22:19)
• locally_constant_on (7 messages, latest: Jun 16 2022 at 17:38)
• In a trivial monoid, everything is a unit (37 messages, latest: Jun 16 2022 at 14:23)
• Restriction of monoid_hom to units? (8 messages, latest: Jun 16 2022 at 13:54)
• Computing nat_degrees of polynomials (38 messages, latest: Jun 16 2022 at 08:01)
• First isomorphism theorem for abelian categories (2 messages, latest: Jun 16 2022 at 07:28)
• category-theoretic triviality (11 messages, latest: Jun 16 2022 at 01:47)
• Indeterminate Integral (13 messages, latest: Jun 15 2022 at 17:49)
• div by p_adic_val_nat is coprime (19 messages, latest: Jun 15 2022 at 15:12)
• Normalizing a vector (10 messages, latest: Jun 15 2022 at 11:19)
• ✔ Explicit zeta and beta reductions (5 messages, latest: Jun 14 2022 at 21:31)
• Explicit zeta and beta reductions (2 messages, latest: Jun 14 2022 at 19:15)
• is_atomistic submodule (13 messages, latest: Jun 14 2022 at 18:10)
• Inserting into is_scalar_tower (11 messages, latest: Jun 13 2022 at 22:25)
• category theory: isomorphisms between images (16 messages, latest: Jun 11 2022 at 09:34)
• Dimension of an affine space (14 messages, latest: Jun 10 2022 at 22:05)
• When does a functor preserve finite (co)limits? (4 messages, latest: Jun 10 2022 at 18:56)
• direct_sum and sum (2 messages, latest: Jun 10 2022 at 14:51)
• Making finset.sum into an explicit sum (20 messages, latest: Jun 09 2022 at 09:59)
• Equiv version of function.swap (7 messages, latest: Jun 09 2022 at 07:37)
• Definitional equality (37 messages, latest: Jun 08 2022 at 01:45)
• ✔ Symmetric group? (4 messages, latest: Jun 07 2022 at 20:23)
• Stacking matrices (5 messages, latest: Jun 06 2022 at 19:13)
• epi_of_comp_epi_of_mono (11 messages, latest: Jun 05 2022 at 11:54)
• ✔ multiset equivalent of is_absolute_value.abv_sum (1 message, latest: Jun 04 2022 at 14:26)
• multiset equivalent of is_absolute_value.abv_sum (3 messages, latest: Jun 04 2022 at 12:52)
• ✔ fin.next (1 message, latest: Jun 03 2022 at 18:00)
• ✔ cases on fin 1 (11 messages, latest: Jun 03 2022 at 14:16)
• div_mul_div_comm for nat (9 messages, latest: Jun 03 2022 at 11:25)
• A functor is additive iff… (2 messages, latest: Jun 02 2022 at 19:19)
• Cyclotomic extensions of finite fields are finite (13 messages, latest: Jun 02 2022 at 07:33)
• cases on fin 1 (4 messages, latest: Jun 02 2022 at 03:43)
• Statements about finite rings (15 messages, latest: Jun 01 2022 at 15:59)
• Standard basis (7 messages, latest: Jun 01 2022 at 14:34)
• Existence of elements of order p in a group (29 messages, latest: May 31 2022 at 07:22)
• false_of_lt_of_lt (3 messages, latest: May 30 2022 at 17:30)
• equivalence of two definitions of span (9 messages, latest: May 30 2022 at 16:17)
• cancelling an isomorphism in a concrete abelian category (1 message, latest: May 30 2022 at 12:26)
• ✔ proof refiner (2 messages, latest: May 30 2022 at 03:34)
• multiset.prod_congr (1 message, latest: May 30 2022 at 01:52)
• Relation between the integral of a function and derivative (21 messages, latest: May 29 2022 at 23:12)
• ✔ Set of subsets of t is equivalent to set t (1 message, latest: May 29 2022 at 21:20)
• Set of subsets of t is equivalent to set t (19 messages, latest: May 29 2022 at 21:00)
• proof refiner (7 messages, latest: May 29 2022 at 19:03)
• ✔ cycle.next and list.next (1 message, latest: May 28 2022 at 22:44)
• cycle.next and list.next (3 messages, latest: May 28 2022 at 21:37)
• ✔ square root of 1 (15 messages, latest: May 28 2022 at 18:24)
• Weak dual with discrete topology (8 messages, latest: May 26 2022 at 19:43)
• ✔ simple(?) summable lemma (4 messages, latest: May 26 2022 at 18:35)
• has_sum for consecutive reciprocals (5 messages, latest: May 26 2022 at 00:33)
• Semiconjugate matrices (17 messages, latest: May 25 2022 at 20:21)
• Lemmas about nat / list / finset (28 messages, latest: May 25 2022 at 00:06)
• nat powers of probabilities (22 messages, latest: May 23 2022 at 23:48)
• Structure theorem for finite(ly generated) abelian groups? (9 messages, latest: May 23 2022 at 16:34)
• (fin (n + 1) → β) ≃ β × (fin n → β) (8 messages, latest: May 23 2022 at 11:39)
• ✔ Regular expression reversal (4 messages, latest: May 23 2022 at 10:06)
• Similarities (36 messages, latest: May 23 2022 at 00:06)
• Extensions of finite fields are Galois? (7 messages, latest: May 22 2022 at 13:51)
• The nth cyclotomic field has a prim. nth root of unity (13 messages, latest: May 21 2022 at 19:08)
• multiplication by a unit is injective (9 messages, latest: May 20 2022 at 22:23)
• closed graph theorem (15 messages, latest: May 20 2022 at 16:56)
• isolated zeros (2 messages, latest: May 19 2022 at 23:15)
• Riesz-Markov-Kakutani representation theorem (2 messages, latest: May 19 2022 at 22:52)
• ✔ Shifting sums (2 messages, latest: May 19 2022 at 11:14)
• Shifting sums (5 messages, latest: May 19 2022 at 09:35)
• preorder on ulift (45 messages, latest: May 18 2022 at 18:06)
• finset proof (22 messages, latest: May 18 2022 at 02:57)
• Discrete Fourier transform (20 messages, latest: May 17 2022 at 23:09)
• set equality (9 messages, latest: May 17 2022 at 16:50)
• Working on the projective line (24 messages, latest: May 16 2022 at 16:40)
• dot_product as inner_product_space (5 messages, latest: May 15 2022 at 20:45)
• Basic set_of lemmas (3 messages, latest: May 15 2022 at 19:31)
• ite_then_ite (16 messages, latest: May 14 2022 at 13:33)
• finset semiring (22 messages, latest: May 13 2022 at 09:44)
• (in)finite binary trees (4 messages, latest: May 12 2022 at 18:29)
• double categories (6 messages, latest: May 12 2022 at 14:09)
• monotone convergence for real sequences (3 messages, latest: May 11 2022 at 20:12)
• Finite field extensions (7 messages, latest: May 10 2022 at 11:09)
• Simpler proof of injectivity {0,1,-1} –> R? (15 messages, latest: May 10 2022 at 10:19)
• ✔ degree of a polynomial (13 messages, latest: May 09 2022 at 11:52)
• equiv_embedding_image (4 messages, latest: May 09 2022 at 11:44)
• coercion into algebraic closure? (28 messages, latest: May 09 2022 at 09:09)
• comp_assoc (5 messages, latest: May 09 2022 at 06:46)
• ✔ using tendsto (11 messages, latest: May 08 2022 at 21:29)
• ✔ prime factorisation (7 messages, latest: May 08 2022 at 20:36)
• using tendsto (7 messages, latest: May 08 2022 at 20:09)
• Riemann Mapping Theorem (10 messages, latest: May 08 2022 at 19:00)
• prime factorisation (7 messages, latest: May 08 2022 at 18:30)
• multiplicity_gcd (9 messages, latest: May 08 2022 at 16:24)
• Why are there two transitive closures? (20 messages, latest: May 08 2022 at 07:19)
• ✔ Lean equivalent to Coq programs? (10 messages, latest: May 08 2022 at 07:00)
• degree of a polynomial (8 messages, latest: May 07 2022 at 18:13)
• inv_of_inj (12 messages, latest: May 07 2022 at 17:15)
• simple function from finite restriction (4 messages, latest: May 06 2022 at 23:14)
• Lean equivalent to Coq programs? (13 messages, latest: May 06 2022 at 20:11)
• Hom-tensor adjunction? (10 messages, latest: May 06 2022 at 16:54)
• ae measurable condition (14 messages, latest: May 06 2022 at 13:29)
• Nonconstant holomorphic functions are open maps (7 messages, latest: May 06 2022 at 13:23)
• Special Linear Groups (16 messages, latest: May 06 2022 at 03:49)
• Currying smooth maps (1 message, latest: May 05 2022 at 13:32)
• is_atomic_of_well_founded (3 messages, latest: May 05 2022 at 06:32)
• Total variation distance on pmf (2 messages, latest: May 04 2022 at 20:22)
• algebra_map clm (6 messages, latest: May 04 2022 at 15:13)
• finsupp.nonzero_iff_exist (22 messages, latest: May 04 2022 at 12:49)
• log over rpow (10 messages, latest: May 03 2022 at 19:36)
• Injectivity of arrow type constructor (20 messages, latest: May 03 2022 at 18:30)
• limit of a sum over nat (10 messages, latest: May 03 2022 at 15:29)
• Endomorphism of ring over itself (4 messages, latest: May 03 2022 at 14:30)
• binary for nnreal (6 messages, latest: May 03 2022 at 00:16)
• Tor (7 messages, latest: May 02 2022 at 18:06)
• ✔ lcm_pos_pos (1 message, latest: May 02 2022 at 18:00)
• ✔ Frobenius norm (10 messages, latest: May 02 2022 at 17:56)
• strictly between squares –> not a square? (13 messages, latest: May 02 2022 at 15:55)
• additive functors preserve binary biproducts (8 messages, latest: May 02 2022 at 15:12)
• monotone_on.mono (7 messages, latest: May 02 2022 at 07:43)
• a fact about equivalences built fiber-wise (9 messages, latest: May 02 2022 at 00:03)
• set.card_to_finset_prod (7 messages, latest: May 01 2022 at 22:39)
• Relating the categorical product and the normal product (23 messages, latest: May 01 2022 at 11:47)
• a fact about cardinalities of preimages (1 message, latest: May 01 2022 at 07:58)
• ✔ bijective function between types of equal cardinality (5 messages, latest: May 01 2022 at 01:38)
• bijective function between types of equal cardinality (7 messages, latest: May 01 2022 at 00:15)
• Does this theorem exist? (1 message, latest: Apr 30 2022 at 22:57)
• subrelation on more than one type (7 messages, latest: Apr 30 2022 at 20:32)
• ✔ Understanding local context (7 messages, latest: Apr 30 2022 at 18:40)
• finset.sum (5 messages, latest: Apr 30 2022 at 11:05)
• linear_map congr (13 messages, latest: Apr 29 2022 at 16:08)
• Sum as integral (3 messages, latest: Apr 29 2022 at 12:28)
• finite_dimensional_of_injective (8 messages, latest: Apr 29 2022 at 10:22)
• Cauchy-Schwarz (22 messages, latest: Apr 29 2022 at 09:52)
• ✔ Cantor's diagonal theorem (11 messages, latest: Apr 29 2022 at 00:51)
• s equiv s.to_finset (5 messages, latest: Apr 28 2022 at 10:15)
• Resultant (2 messages, latest: Apr 27 2022 at 15:16)
• sum of row sums equals sum of column sums (17 messages, latest: Apr 27 2022 at 11:57)
• Distributivity of ite (1 message, latest: Apr 27 2022 at 10:00)
• pi.nonempty (11 messages, latest: Apr 26 2022 at 23:45)
• Type-ascript to a Euclidean space (22 messages, latest: Apr 26 2022 at 16:31)
• Link to files (8 messages, latest: Apr 26 2022 at 13:13)
• representations of k-algebras (9 messages, latest: Apr 26 2022 at 13:07)
• making implicit variable explicit in output (20 messages, latest: Apr 26 2022 at 07:29)
• Finiteness of tensor product (7 messages, latest: Apr 26 2022 at 06:54)
• lintegral_coe_eq_coe_integral (7 messages, latest: Apr 25 2022 at 20:38)
• Zero-dimensional space (1 message, latest: Apr 25 2022 at 19:09)
• lcm_pos_pos (3 messages, latest: Apr 25 2022 at 17:05)
• maps_to_prod (3 messages, latest: Apr 25 2022 at 13:02)
• boundedness of sums (4 messages, latest: Apr 25 2022 at 10:41)
• PL theory stuff (3 messages, latest: Apr 24 2022 at 11:01)
• ✔ Linear map from the base ring (1 message, latest: Apr 22 2022 at 13:40)
• add_min_max (5 messages, latest: Apr 22 2022 at 11:34)
• ✔ mod_pow_mod (2 messages, latest: Apr 22 2022 at 09:38)
• Linear map from the base ring (5 messages, latest: Apr 22 2022 at 03:29)
• every finite type admits a linear order (10 messages, latest: Apr 21 2022 at 18:16)
• ✔ Equip a type with the discrete topology (1 message, latest: Apr 21 2022 at 15:04)
• sum_ite_eq_extract (21 messages, latest: Apr 21 2022 at 14:49)
• Switch limit and derivative given uniform convergence (5 messages, latest: Apr 20 2022 at 18:05)
• mod_pow_mod (17 messages, latest: Apr 20 2022 at 15:25)
• Finset filter map (2 messages, latest: Apr 19 2022 at 20:00)
• arclength of a function (7 messages, latest: Apr 19 2022 at 18:56)
• ring.inverse is continuous (38 messages, latest: Apr 19 2022 at 14:40)
• Integers of norm at most one (18 messages, latest: Apr 19 2022 at 12:50)
• Trace of tensor product (2 messages, latest: Apr 19 2022 at 12:33)
• finset.sup_mul_left (24 messages, latest: Apr 19 2022 at 10:37)
• Localization of ℤ at p as a subring of ℚ with hom. to ℤ/pℤ? (30 messages, latest: Apr 19 2022 at 02:02)
• use tactic (21 messages, latest: Apr 18 2022 at 22:24)
• lcm and divisors (9 messages, latest: Apr 18 2022 at 08:35)
• filter map₂ as map (30 messages, latest: Apr 17 2022 at 21:43)
• set.any (10 messages, latest: Apr 17 2022 at 20:05)
• sum_sum (7 messages, latest: Apr 17 2022 at 15:15)
• ✔ Product of sums as double sum? (3 messages, latest: Apr 16 2022 at 18:31)
• ✔ inversion of a group with zero as a monoid_with_zero_hom? (2 messages, latest: Apr 16 2022 at 18:21)
• inversion of a group with zero as a monoid_with_zero_hom? (3 messages, latest: Apr 16 2022 at 18:14)
• ✔ not_not + mt (4 messages, latest: Apr 16 2022 at 16:40)
• non-unital comm (semi)ring (7 messages, latest: Apr 16 2022 at 06:02)
• rat.mul_eq (3 messages, latest: Apr 15 2022 at 18:55)
• Elements of finite fields of char 2 are squares (13 messages, latest: Apr 15 2022 at 18:50)
• lcm equal first iff second divides first (8 messages, latest: Apr 15 2022 at 12:02)
• ✔ Continuous linear map finite dimension (10 messages, latest: Apr 15 2022 at 10:17)
• ✔ a - b = -b + a (11 messages, latest: Apr 15 2022 at 07:22)
• power of product in comm_monoid (4 messages, latest: Apr 14 2022 at 15:56)
• The "other kind" of commutator (7 messages, latest: Apr 14 2022 at 14:24)
• C(S, V) complete and separated (9 messages, latest: Apr 14 2022 at 14:11)
• Lp for 0<p<1 (17 messages, latest: Apr 14 2022 at 07:46)
• Localization inside of fraction field (3 messages, latest: Apr 13 2022 at 16:20)
• rat-normed space (8 messages, latest: Apr 13 2022 at 13:18)
• filter.has_scalar missing? (46 messages, latest: Apr 12 2022 at 23:19)
• bijection range n → zmod n? (152 messages, latest: Apr 12 2022 at 22:17)
• A finite field has at least two elements (10 messages, latest: Apr 12 2022 at 18:30)
• square root of 1 (7 messages, latest: Apr 11 2022 at 20:21)
• ✔ Find the nth element of an ordered finset (2 messages, latest: Apr 11 2022 at 13:25)
• Find the nth element of an ordered finset (6 messages, latest: Apr 11 2022 at 13:25)
• monoid_hom from mul_hom? (15 messages, latest: Apr 11 2022 at 13:07)
• coefficients of sum a(n) X^n (3 messages, latest: Apr 11 2022 at 04:03)
• Even power of -1 (16 messages, latest: Apr 09 2022 at 17:54)
• pfun to total function (11 messages, latest: Apr 09 2022 at 16:46)
• ✔ Indicator of intersection (5 messages, latest: Apr 09 2022 at 14:33)
• Indicator of intersection (6 messages, latest: Apr 09 2022 at 12:03)
• Working with polynomial factorizations (132 messages, latest: Apr 09 2022 at 06:52)
• Sequence limit (4 messages, latest: Apr 08 2022 at 15:41)
• Tensor maps (15 messages, latest: Apr 08 2022 at 02:24)
• Finiteness of subalgebra of algebraic extensions of F_p (9 messages, latest: Apr 07 2022 at 15:09)
• Continuity of integral for a sub-sigma-field (10 messages, latest: Apr 07 2022 at 14:38)
• ✔ a dependent version of finset.bUnion? (5 messages, latest: Apr 07 2022 at 12:08)
• traversing an expression making replacements (3 messages, latest: Apr 07 2022 at 09:04)
• ideal generator element of ideal (27 messages, latest: Apr 06 2022 at 20:13)
• appended lists equal of length equal (11 messages, latest: Apr 06 2022 at 15:02)
• Sequence density (2 messages, latest: Apr 06 2022 at 15:02)
• p-adic valuation (49 messages, latest: Apr 05 2022 at 20:34)
• lemma about when a filter is a pure filter (58 messages, latest: Apr 04 2022 at 17:04)
• a < b ∧ a = b → false (4 messages, latest: Apr 04 2022 at 16:46)
• Finitary scalar product (36 messages, latest: Apr 04 2022 at 13:34)
• ✔ Mapping into a finset product (6 messages, latest: Apr 03 2022 at 02:46)
• word length in a free group (8 messages, latest: Apr 01 2022 at 16:57)
• char_zero instance on polynomials (34 messages, latest: Mar 31 2022 at 15:55)
• Equip a type with the discrete topology (10 messages, latest: Mar 31 2022 at 10:04)
• ✔ category of sheaf is abelian (26 messages, latest: Mar 31 2022 at 02:40)
• ✔ equiv.cast that preserves structure (1 message, latest: Mar 30 2022 at 17:20)
• equiv.cast that preserves structure (8 messages, latest: Mar 30 2022 at 16:20)
• ✔ Almost equal preimages (3 messages, latest: Mar 30 2022 at 15:12)
• ✔ Prove known function is group isomorphism (3 messages, latest: Mar 30 2022 at 13:35)
• Prove known function is group isomorphism (3 messages, latest: Mar 30 2022 at 12:17)
• independent random variables (10 messages, latest: Mar 30 2022 at 09:40)
• ✔ Preimage of normed ball (2 messages, latest: Mar 30 2022 at 09:22)
• Preimage of normed ball (11 messages, latest: Mar 30 2022 at 09:02)
• Abelian subgroup dividing order (5 messages, latest: Mar 30 2022 at 06:46)
• Determining Integral (11 messages, latest: Mar 30 2022 at 00:45)
• neg_zero for has_distrib_neg (7 messages, latest: Mar 29 2022 at 20:30)
• hom.op_inv (20 messages, latest: Mar 29 2022 at 19:48)
• nat.antidiagonal for pi types (16 messages, latest: Mar 29 2022 at 12:35)
• basis..sum_extend_extends (2 messages, latest: Mar 29 2022 at 10:22)
• num_3_dvd_of_mod_9_eq_3_or_6 (3 messages, latest: Mar 29 2022 at 07:52)
• Q is injective (3 messages, latest: Mar 28 2022 at 22:18)
• algebra ℕ[X] R[X] (41 messages, latest: Mar 28 2022 at 10:13)
• Expressing x⁻¹ from a polynomial equality (4 messages, latest: Mar 28 2022 at 09:32)
• Mapping into a finset product (15 messages, latest: Mar 27 2022 at 23:27)
• ✔ Cartesian product in finset (1 message, latest: Mar 27 2022 at 22:28)
• Cartesian product in finset (6 messages, latest: Mar 27 2022 at 22:07)
• mixed version of ssubset_trans (14 messages, latest: Mar 27 2022 at 15:59)
• Stacks definition of abelian cats (43 messages, latest: Mar 27 2022 at 04:05)
• is_prime_field (13 messages, latest: Mar 26 2022 at 18:29)
• polynomial.comp_prod (27 messages, latest: Mar 26 2022 at 17:30)
• symmetric difference / disjunctive union of sets (47 messages, latest: Mar 26 2022 at 17:02)
• closure of element of infinite order (15 messages, latest: Mar 25 2022 at 17:14)
• Named deferred goals (11 messages, latest: Mar 25 2022 at 14:45)
• char_p instance on polynomials (5 messages, latest: Mar 25 2022 at 12:07)
• ✔ Dimension of intersection (13 messages, latest: Mar 24 2022 at 20:10)
• polynomial preimage of nonzero is dense (19 messages, latest: Mar 24 2022 at 18:48)
• Bounded conditional supremum (44 messages, latest: Mar 24 2022 at 14:09)
• finsupp total eq sum (14 messages, latest: Mar 24 2022 at 09:15)
• groups of order p² (5 messages, latest: Mar 23 2022 at 21:45)
• p-adic norm of (a : int) = 1 from p not dividing a? (14 messages, latest: Mar 23 2022 at 20:48)
• Independent iff independent (4 messages, latest: Mar 23 2022 at 08:17)
• sup metric convergence is uniform convergence (8 messages, latest: Mar 23 2022 at 04:18)
• Smallness from a cardinal bound (3 messages, latest: Mar 22 2022 at 20:36)
• more inductions for int (52 messages, latest: Mar 22 2022 at 18:36)
• hom from mul monoid to add monoid (4 messages, latest: Mar 22 2022 at 08:14)
• Applying continuous linear map (5 messages, latest: Mar 21 2022 at 21:31)
• ✔ scaling of union (5 messages, latest: Mar 21 2022 at 16:52)
• multiplicity of derivative (12 messages, latest: Mar 21 2022 at 11:57)
• Partial derivatives' chain rule & product rule (3 messages, latest: Mar 21 2022 at 11:32)
• int.gcd_add_self_right (3 messages, latest: Mar 20 2022 at 23:07)
• filter.comap₂ (4 messages, latest: Mar 20 2022 at 17:25)
• finding instance declaration (20 messages, latest: Mar 19 2022 at 21:25)
• finset of functions (4 messages, latest: Mar 19 2022 at 20:57)
• Totally boundedness (2 messages, latest: Mar 19 2022 at 15:44)
• Realizing the Hausdorff distance (19 messages, latest: Mar 19 2022 at 01:19)
• Splitting lemma for modules (7 messages, latest: Mar 18 2022 at 23:27)
• Reference a part of an expression (19 messages, latest: Mar 18 2022 at 23:26)
• nilpotency in finite groups (14 messages, latest: Mar 18 2022 at 22:54)
• ✔ emetric.continuous_at_iff (2 messages, latest: Mar 18 2022 at 18:50)
• emetric.continuous_at_iff (3 messages, latest: Mar 18 2022 at 16:46)
• triangle equality if arg is equal (13 messages, latest: Mar 17 2022 at 23:43)
• ✔ nat.lt_iff_eq_succ (6 messages, latest: Mar 16 2022 at 22:18)
• is_closed.smul for fields (12 messages, latest: Mar 16 2022 at 22:16)
• 2 is not a square (37 messages, latest: Mar 16 2022 at 08:02)
• tensor products commute with direct limits (57 messages, latest: Mar 16 2022 at 06:58)
• Integral of 1/sqrt(x) (24 messages, latest: Mar 16 2022 at 05:19)
• nat.lt_iff_eq_succ (5 messages, latest: Mar 15 2022 at 23:53)
• Hom(Z,A) (11 messages, latest: Mar 14 2022 at 23:09)
• stream events (2 messages, latest: Mar 14 2022 at 20:02)
• Coprimeness of products from pairwise coprimeness (16 messages, latest: Mar 14 2022 at 12:31)
• Functions into sums (32 messages, latest: Mar 14 2022 at 11:37)
• checking if function is a probability measure (8 messages, latest: Mar 13 2022 at 20:13)
• mkq = 0 iff (8 messages, latest: Mar 13 2022 at 08:13)
• ✔ clearing denominators (1 message, latest: Mar 12 2022 at 20:13)
• clearing denominators (5 messages, latest: Mar 12 2022 at 20:13)
• transferring topological properties along homeomorphisms (16 messages, latest: Mar 12 2022 at 15:16)
• classes for symmetric transitive relation (22 messages, latest: Mar 11 2022 at 16:05)
• Injectivity of quiver.hom.op (5 messages, latest: Mar 11 2022 at 14:39)
• Injectivity of functor.op (10 messages, latest: Mar 11 2022 at 13:05)
• tendsto.units (3 messages, latest: Mar 10 2022 at 22:17)
• zmod.nat_cast_eq_iff (11 messages, latest: Mar 10 2022 at 17:43)
• linear_map.eq_locus (5 messages, latest: Mar 10 2022 at 17:42)
• ✔ cartesian product (8 messages, latest: Mar 10 2022 at 15:37)
• cartesian product (5 messages, latest: Mar 10 2022 at 15:11)
• fin n with saturating addition (19 messages, latest: Mar 10 2022 at 13:20)
• polynomial.map as algebra hom (10 messages, latest: Mar 10 2022 at 13:05)
• nat abs or (2 messages, latest: Mar 10 2022 at 01:34)
• injection to show cardinality inquality (5 messages, latest: Mar 09 2022 at 22:34)
• A-B (14 messages, latest: Mar 09 2022 at 18:48)
• ✔ equivalence of category preserves (co)limits (4 messages, latest: Mar 09 2022 at 12:50)
• Range equiv quotient by ker (7 messages, latest: Mar 09 2022 at 11:17)
• Power of two (22 messages, latest: Mar 08 2022 at 11:23)
• ✔ nat_mul_comm (7 messages, latest: Mar 08 2022 at 10:54)
• ✔ nat.ceil on nnreal ? (1 message, latest: Mar 07 2022 at 21:46)
• nat.ceil on nnreal ? (26 messages, latest: Mar 07 2022 at 16:15)
• unbounded function (1 message, latest: Mar 07 2022 at 15:08)
• Isometry group of pseudo_emetric space splits (1 message, latest: Mar 06 2022 at 09:36)
• Multiplicity in the naturals (29 messages, latest: Mar 05 2022 at 06:35)
• geom_sum (X n) is monic (11 messages, latest: Mar 04 2022 at 14:39)
• summable.single_le_tsum (4 messages, latest: Mar 04 2022 at 14:07)
• Completeness of padics (25 messages, latest: Mar 03 2022 at 21:17)
• omega < aleph (n+1) (19 messages, latest: Mar 03 2022 at 19:53)
• cancel division in polynomials (8 messages, latest: Mar 02 2022 at 18:38)
• nnnorm and complex (3 messages, latest: Mar 02 2022 at 17:24)
• (Co)completion of a category (11 messages, latest: Mar 02 2022 at 15:54)
• C1 on product (5 messages, latest: Mar 02 2022 at 13:34)
• submodule.sup basic lemma (9 messages, latest: Mar 02 2022 at 10:44)
• ✔ prod.fst as a hom (3 messages, latest: Mar 01 2022 at 21:05)
• int.to_nat_eq_zero (8 messages, latest: Mar 01 2022 at 20:17)
• ✔ Creating a example perm (1 message, latest: Mar 01 2022 at 19:36)
• undergrad todo trivial target Linear Algebra / Duality / (5 messages, latest: Mar 01 2022 at 18:58)
• computable operations for rational numbers (8 messages, latest: Mar 01 2022 at 18:44)
• difference of squares of commuting elements (7 messages, latest: Mar 01 2022 at 12:04)
• universal property of sheafification (on topological spaces) (15 messages, latest: Mar 01 2022 at 10:57)
• Completeness of direct sums of Hilbert spaces? (4 messages, latest: Mar 01 2022 at 03:45)
• Creating a example perm (3 messages, latest: Mar 01 2022 at 00:41)
• topological embeddings of orders (2 messages, latest: Feb 28 2022 at 17:12)
• subtype.coe_fn_coe (4 messages, latest: Feb 28 2022 at 13:09)
• the law of a random variable is a probability measure (17 messages, latest: Feb 28 2022 at 02:24)
• S - {x} ? (8 messages, latest: Feb 27 2022 at 20:38)
• Bump functions (32 messages, latest: Feb 27 2022 at 20:22)
• ✔ List repeat (4 messages, latest: Feb 27 2022 at 18:06)
• List repeat (3 messages, latest: Feb 27 2022 at 15:18)
• Group Amalgamation (2 messages, latest: Feb 26 2022 at 21:49)
• base change / pullback (10 messages, latest: Feb 26 2022 at 12:10)
• set.sigma (8 messages, latest: Feb 26 2022 at 11:04)
• finset.sum_add (4 messages, latest: Feb 26 2022 at 08:09)
• submodule of free module over PID is free (15 messages, latest: Feb 25 2022 at 16:28)
• ring_equiv.Pi_congr_right (4 messages, latest: Feb 25 2022 at 16:11)
• Minimal polynomial of ζ - 1 (2 messages, latest: Feb 25 2022 at 12:12)
• Finite types (6 messages, latest: Feb 25 2022 at 11:48)
• Frobenius norm (1 message, latest: Feb 24 2022 at 22:52)
• ✔ δ-ɛ continuity for metric spaces (11 messages, latest: Feb 24 2022 at 22:36)
• δ-ɛ continuity for metric spaces (1 message, latest: Feb 24 2022 at 22:02)
• with_zero (multiplicative A) ≃* multiplicative (with_bot A) (32 messages, latest: Feb 24 2022 at 20:01)
• units as a functor (8 messages, latest: Feb 24 2022 at 09:48)
• α ≃ β → option α ≃ option β (3 messages, latest: Feb 24 2022 at 00:35)
• exists_extends of linear_pmap (18 messages, latest: Feb 23 2022 at 21:26)
• Continuous algebra homomorphisms (37 messages, latest: Feb 22 2022 at 19:25)
• continuous bilinear map (14 messages, latest: Feb 22 2022 at 13:21)
• is_iso dist triang (17 messages, latest: Feb 22 2022 at 00:42)
• ✔ nat pow tendsto (3 messages, latest: Feb 22 2022 at 00:01)
• nat pow tendsto (3 messages, latest: Feb 21 2022 at 22:28)
• cokernel_lift_iso_kernel_desc (31 messages, latest: Feb 21 2022 at 21:08)
• At least three elements (28 messages, latest: Feb 21 2022 at 20:06)
• apply function n times (47 messages, latest: Feb 20 2022 at 18:11)
• set to list (16 messages, latest: Feb 20 2022 at 01:32)
• completion of a normed space (14 messages, latest: Feb 19 2022 at 17:39)
• ✔ Lagrange's Theorem (Group theory) (10 messages, latest: Feb 19 2022 at 01:19)
• nnnorm and int.nat_abs (11 messages, latest: Feb 18 2022 at 08:48)
• finset.some (24 messages, latest: Feb 17 2022 at 19:20)
• mul_infi_of_nonneg (3 messages, latest: Feb 17 2022 at 18:06)
• ✔ uncoerce equality (6 messages, latest: Feb 17 2022 at 11:51)
• Uncountable sum diverges (4 messages, latest: Feb 17 2022 at 06:41)
• N ⊓ P as a submodule of N (11 messages, latest: Feb 15 2022 at 08:01)
• Cobordism hypothesis (5 messages, latest: Feb 15 2022 at 04:42)
• Rational basis of a number field (16 messages, latest: Feb 14 2022 at 21:33)
• co-bounded filter (73 messages, latest: Feb 14 2022 at 17:28)
• Holder inequality (3 messages, latest: Feb 14 2022 at 13:39)
• (R →ₗ[R] M) ≃ M (4 messages, latest: Feb 14 2022 at 12:28)
• replacement of finset.sum_hom (7 messages, latest: Feb 13 2022 at 20:44)
• Lifting order structure (7 messages, latest: Feb 13 2022 at 12:07)
• integral sum measure (6 messages, latest: Feb 13 2022 at 01:39)
• finite categories (15 messages, latest: Feb 13 2022 at 01:13)
• Some missing prod stuff (57 messages, latest: Feb 12 2022 at 23:37)
• [generalize at ](topic/generalize.20at.20.html) (3 messages, latest: Feb 12 2022 at 21:27)
• Bijections and Inverses, Cauchy sequence permutations (6 messages, latest: Feb 12 2022 at 20:55)
• primer on set_option (12 messages, latest: Feb 12 2022 at 19:44)
• (no topic) (15 messages, latest: Feb 12 2022 at 10:02)
• Bijections and Inverses (28 messages, latest: Feb 12 2022 at 00:44)
• Functions are unequal if they disagree somewhere (16 messages, latest: Feb 11 2022 at 22:29)
• set.finite of subset range (7 messages, latest: Feb 11 2022 at 15:59)
• elements of an action which fix a set (22 messages, latest: Feb 10 2022 at 09:18)
• ✔ enat.eq_zero_iff_le_zero (8 messages, latest: Feb 09 2022 at 17:47)
• a convex set is null measurable (6 messages, latest: Feb 09 2022 at 15:02)
• ✔ heq_congr? (10 messages, latest: Feb 09 2022 at 06:13)
• polynomial/finsupp to list (3 messages, latest: Feb 09 2022 at 01:51)
• mul_neg, neg_mul (4 messages, latest: Feb 08 2022 at 22:08)
• set α in fintype α (37 messages, latest: Feb 08 2022 at 22:00)
• opinionated formatter à la black (4 messages, latest: Feb 08 2022 at 10:13)
• heq_congr? (5 messages, latest: Feb 08 2022 at 03:10)
• Exactness in opposite category (4 messages, latest: Feb 07 2022 at 18:09)
• [le and eq iff ](topic/le.20and.20eq.20iff.20.html) (7 messages, latest: Feb 07 2022 at 09:22)
• Sub-variables (3 messages, latest: Feb 07 2022 at 08:01)
• subtype as a fintype (12 messages, latest: Feb 06 2022 at 01:17)
• ✔ pi subgroups (22 messages, latest: Feb 05 2022 at 13:48)
• Compact opens (38 messages, latest: Feb 05 2022 at 13:34)
• ✔ Range factorization with subtype? (13 messages, latest: Feb 05 2022 at 08:54)
• Free strict n-categories (6 messages, latest: Feb 05 2022 at 08:08)
• finset.max! (5 messages, latest: Feb 04 2022 at 23:11)
• prod version of nat.coprime.lcm_eq_mul (15 messages, latest: Feb 04 2022 at 22:15)
• ✔ order_dual infi supr (4 messages, latest: Feb 04 2022 at 16:57)
• Wlog in the usual sense (5 messages, latest: Feb 04 2022 at 12:22)
• ✔ Generalization of set.image_inter_on (1 message, latest: Feb 04 2022 at 03:12)
• Generalization of set.image_inter_on (7 messages, latest: Feb 04 2022 at 00:26)
• induction on an index type (20 messages, latest: Feb 03 2022 at 18:47)
• Counterpart of rw for modeq (4 messages, latest: Feb 03 2022 at 18:44)
• pi subgroups (16 messages, latest: Feb 03 2022 at 16:50)
• Lift composition with quot.mk (9 messages, latest: Feb 02 2022 at 21:46)
• Merge (ordered) streams (5 messages, latest: Feb 02 2022 at 17:40)
• Semigroupoidal category (16 messages, latest: Feb 02 2022 at 14:29)
• Bipointed (2 messages, latest: Feb 02 2022 at 10:15)
• transcendence of pi (13 messages, latest: Feb 02 2022 at 09:19)
• zify and divisibility (4 messages, latest: Feb 01 2022 at 21:31)
• Sum of Inf is Inf of sum (14 messages, latest: Feb 01 2022 at 16:43)
• ✔ pi.single but for multiplicative groups (2 messages, latest: Feb 01 2022 at 16:30)
• pi.single but for multiplicative groups (2 messages, latest: Feb 01 2022 at 09:28)
• proving equality of cartesian product (5 messages, latest: Feb 01 2022 at 03:56)
• ✔ fderiv equal to has_fderiv (4 messages, latest: Feb 01 2022 at 00:10)
• Decidable rels on a quotient (5 messages, latest: Jan 29 2022 at 22:35)
• Predicate for an element being an inverse in a comm_monoid (5 messages, latest: Jan 28 2022 at 12:20)
• ✔ Pretty printing of equivalence classes (17 messages, latest: Jan 28 2022 at 04:08)
• Multiset min/max (2 messages, latest: Jan 27 2022 at 20:13)
• product of surjective functions is surjective (7 messages, latest: Jan 27 2022 at 20:07)
• Lindelof spaces (34 messages, latest: Jan 27 2022 at 16:10)
• Pretty printing of equivalence classes (13 messages, latest: Jan 27 2022 at 14:02)
• ✔ injections to equiv (6 messages, latest: Jan 26 2022 at 21:18)
• integral is continuously differentiable (11 messages, latest: Jan 26 2022 at 17:40)
• pw_filter is maximal (5 messages, latest: Jan 26 2022 at 16:29)
• Quotient of a quotient (14 messages, latest: Jan 26 2022 at 14:16)
• ordered_comm_monoid_with_zero (5 messages, latest: Jan 26 2022 at 14:04)
• Least extended natural with witness (5 messages, latest: Jan 26 2022 at 09:38)
• Is this a valid way of defining a typeclass? (146 messages, latest: Jan 26 2022 at 02:09)
• Multiindex notation (14 messages, latest: Jan 25 2022 at 21:03)
• Localization of ordered integral domains (6 messages, latest: Jan 25 2022 at 10:25)
• ✔ ℝ>0 (33 messages, latest: Jan 25 2022 at 07:34)
• show with turnstile (7 messages, latest: Jan 24 2022 at 21:11)
• any cover admits a countable subcover (9 messages, latest: Jan 24 2022 at 18:48)
• Complete destruction tactic (35 messages, latest: Jan 24 2022 at 12:58)
• Complement is strictly antitone (5 messages, latest: Jan 23 2022 at 21:17)
• Bitopological spaces (1 message, latest: Jan 21 2022 at 21:20)
• char is some prime given prime is zero (4 messages, latest: Jan 21 2022 at 14:09)
• ✔ inv_mul_eq_iff_eq_mul₀ for ennreal (1 message, latest: Jan 20 2022 at 14:38)
• data.nat.parity (10 messages, latest: Jan 20 2022 at 14:31)
• tactic for proving iff (1 message, latest: Jan 20 2022 at 12:45)
• ✔ Continuous linear map to normed group hom (1 message, latest: Jan 20 2022 at 08:57)
• inv_mul_eq_iff_eq_mul₀ for ennreal (5 messages, latest: Jan 20 2022 at 03:04)
• weaker conditions for showing algebraically closed (3 messages, latest: Jan 19 2022 at 21:33)
• Continuous linear map to normed group hom (17 messages, latest: Jan 19 2022 at 18:29)
• bUnion for set (28 messages, latest: Jan 18 2022 at 20:57)
• Mochizuki proof of abc conjecture (3 messages, latest: Jan 16 2022 at 16:42)
• ✔ some power of 1/2 less than a positive real (4 messages, latest: Jan 16 2022 at 09:26)
• ✔ set singletons injective (2 messages, latest: Jan 15 2022 at 11:00)
• Thickening and closed thickening (19 messages, latest: Jan 14 2022 at 23:12)
• injections to equiv (61 messages, latest: Jan 14 2022 at 17:38)
• Union of singletons (4 messages, latest: Jan 14 2022 at 17:20)
• set singletons injective (8 messages, latest: Jan 14 2022 at 15:43)
• finsupp.map_range (2 messages, latest: Jan 14 2022 at 06:42)
• linear maps of polynomials (21 messages, latest: Jan 13 2022 at 20:22)
• fintype arrow (10 messages, latest: Jan 13 2022 at 17:01)
• nat-bezout (29 messages, latest: Jan 13 2022 at 14:52)
• pow_cancel_left (4 messages, latest: Jan 13 2022 at 10:37)
• random number generator (18 messages, latest: Jan 13 2022 at 04:27)
• dfinsupp sum ite (9 messages, latest: Jan 12 2022 at 22:37)
• Disjoint union of posets (96 messages, latest: Jan 11 2022 at 22:52)
• Epi iff surjective in Ab. (2 messages, latest: Jan 11 2022 at 22:41)
• function on a union (3 messages, latest: Jan 11 2022 at 15:58)
• min and max of finsupps (16 messages, latest: Jan 11 2022 at 15:42)
• Generalization of mul_eq_one_comm (15 messages, latest: Jan 11 2022 at 13:52)
• mv_polynomial.total_degree of sum (7 messages, latest: Jan 11 2022 at 12:48)
• Disjoint union of finsets (10 messages, latest: Jan 11 2022 at 10:26)
• sub_group_with_zero (4 messages, latest: Jan 11 2022 at 07:37)
• Order on a quotient group (1 message, latest: Jan 10 2022 at 21:01)
• ✔ polynomials spanned by monomials (2 messages, latest: Jan 10 2022 at 11:43)
• polynomials spanned by monomials (4 messages, latest: Jan 10 2022 at 09:05)
• mul_sup for non-negative reals (17 messages, latest: Jan 09 2022 at 18:44)
• 2^n >= n^m (48 messages, latest: Jan 07 2022 at 22:31)
• Regressive induction (15 messages, latest: Jan 07 2022 at 20:23)
• mccoy's theorem (2 messages, latest: Jan 07 2022 at 20:03)
• enumerate nonempty lists (16 messages, latest: Jan 07 2022 at 14:59)
• tactic for specificed commutativity and associativity? (3 messages, latest: Jan 07 2022 at 02:06)
• generalised eventually_at_top (14 messages, latest: Jan 06 2022 at 18:40)
• antiderivative (37 messages, latest: Jan 06 2022 at 18:11)
• Abstracting * and / (21 messages, latest: Jan 06 2022 at 14:00)
• Minimal elements and descending chains (33 messages, latest: Jan 06 2022 at 09:42)
• Criterion for set.finite from finsets (3 messages, latest: Jan 05 2022 at 20:13)
• set.card_to_finset_univ (32 messages, latest: Jan 04 2022 at 23:43)
• real.log in other base (6 messages, latest: Jan 04 2022 at 21:46)
• opposite multiplication for subgroups (7 messages, latest: Jan 04 2022 at 16:20)
• ✔ f^[n] x = x (13 messages, latest: Jan 03 2022 at 04:56)
• Ring for vector spaces (17 messages, latest: Jan 02 2022 at 22:33)
• Minimal relation satisfying trans_gen (14 messages, latest: Jan 02 2022 at 20:09)
• nonemptiness tactic (5 messages, latest: Jan 02 2022 at 17:06)
• f^[n] x = x (4 messages, latest: Jan 01 2022 at 14:03)
• Prop-valued "I am a finite type" (3 messages, latest: Dec 31 2021 at 17:32)
• Multiset functor map with erase_dup (17 messages, latest: Dec 31 2021 at 16:22)
• x in subobject (O(K)) -> (x : K) in subobject K (4 messages, latest: Dec 30 2021 at 22:20)
• flip eq curry swap uncurry (2 messages, latest: Dec 30 2021 at 18:08)
• nat.nat_one_eq_one (16 messages, latest: Dec 30 2021 at 01:13)
• tensor calculus (4 messages, latest: Dec 29 2021 at 16:10)
• (l₁ S).map σ ≤ l₂ (S.map ⇑σ) (31 messages, latest: Dec 28 2021 at 23:31)
• eventually eventually (11 messages, latest: Dec 28 2021 at 22:18)
• Dual to option.mem_unique? (12 messages, latest: Dec 28 2021 at 22:09)
• ✔ Bounds along filters (11 messages, latest: Dec 28 2021 at 02:17)
• Additive is_scalar_tower (13 messages, latest: Dec 27 2021 at 21:08)
• Unique factorization of complex polynomials (8 messages, latest: Dec 27 2021 at 16:33)
• Continuous bijective from compact to T1 implies homeomorphis (24 messages, latest: Dec 27 2021 at 15:28)
• ✔ ultrafilter is principal if it contains a finite set (2 messages, latest: Dec 27 2021 at 14:57)
• α →* β typeclasses (8 messages, latest: Dec 27 2021 at 11:13)
• ultrafilter is principal if it contains a finite set (13 messages, latest: Dec 27 2021 at 09:29)
• -1 ^ n (15 messages, latest: Dec 26 2021 at 03:00)
• ✔ Measurable of constant on intervals (1 message, latest: Dec 25 2021 at 18:19)
• Measurable of constant on intervals (4 messages, latest: Dec 25 2021 at 18:11)
• U' ⊗ V ≃ Hom(U, V) (5 messages, latest: Dec 25 2021 at 14:41)
• preorder (opposite X) (30 messages, latest: Dec 25 2021 at 01:17)
• ✔ every type can be well-ordered (3 messages, latest: Dec 24 2021 at 02:44)
• every type can be well-ordered (1 message, latest: Dec 24 2021 at 02:27)
• Functoriality of finset (25 messages, latest: Dec 23 2021 at 22:35)
• Power series (21 messages, latest: Dec 23 2021 at 19:49)
• Long line (3 messages, latest: Dec 23 2021 at 17:11)
• Multiply is_lub (9 messages, latest: Dec 23 2021 at 07:20)
• filtered finset cardinality (3 messages, latest: Dec 22 2021 at 22:02)
• [Writing n as p^km](topic/Writing.20n.20as.20p.5Ekm.html) (20 messages, latest: Dec 22 2021 at 18:44)
• sum nonnegative iff elements nonnegative (5 messages, latest: Dec 22 2021 at 10:12)
• Applying ring_equiv.to_ring_hom (9 messages, latest: Dec 22 2021 at 00:07)
• Lifting is_empty instance (6 messages, latest: Dec 21 2021 at 23:55)
• fin n combinatorics (18 messages, latest: Dec 21 2021 at 15:39)
• coinduced/product topologies (16 messages, latest: Dec 20 2021 at 23:16)
• Dependent forall_congr (5 messages, latest: Dec 20 2021 at 23:13)
• Compositum of finite field extensions is finite (24 messages, latest: Dec 20 2021 at 22:34)
• polynomial.eval_eval₂ (12 messages, latest: Dec 20 2021 at 01:02)
• normal extension = normal subgroup (2 messages, latest: Dec 20 2021 at 00:11)
• finsupp.pi (30 messages, latest: Dec 19 2021 at 19:38)
• Computational sum_four_squares (27 messages, latest: Dec 19 2021 at 16:23)
• Normal closure of subfield exists and is finite dimensional (3 messages, latest: Dec 19 2021 at 12:51)
• strict_mono on int (4 messages, latest: Dec 19 2021 at 11:47)
• exists a unique nth element of fin n (5 messages, latest: Dec 18 2021 at 00:18)
• naming help (14 messages, latest: Dec 17 2021 at 20:47)
• Equivalences between containers induced elementwise (13 messages, latest: Dec 17 2021 at 18:03)
• card_filter_fin_lt (5 messages, latest: Dec 17 2021 at 16:01)
• not xor (6 messages, latest: Dec 17 2021 at 12:57)
• Preorder on dfinsupp (6 messages, latest: Dec 17 2021 at 12:25)
• finset.to_list sum (34 messages, latest: Dec 17 2021 at 09:54)
• ✔ monoid_hom from additive to multiplicative structures (2 messages, latest: Dec 17 2021 at 04:14)
• monoid_hom from additive to multiplicative structures (11 messages, latest: Dec 17 2021 at 00:35)
• sqrt (r : \C) * sqrt r (5 messages, latest: Dec 16 2021 at 22:39)
• Algebras over Witt vectors (3 messages, latest: Dec 16 2021 at 21:43)
• ✔ formal power series (2 messages, latest: Dec 16 2021 at 16:07)
• has_pow_of_has_one_has_mul (12 messages, latest: Dec 16 2021 at 15:33)
• finite domain -> finsupp (3 messages, latest: Dec 16 2021 at 13:22)
• computable_pred and primcodable ℚ (4 messages, latest: Dec 16 2021 at 13:18)
• ✔ Quotient of Pi type equivalent to Pi of quotient type (2 messages, latest: Dec 16 2021 at 05:02)
• Quotient of Pi type equivalent to Pi of quotient type (1 message, latest: Dec 16 2021 at 02:21)
• Concrete fraction ring of int (31 messages, latest: Dec 15 2021 at 22:24)
• formal power series (1 message, latest: Dec 15 2021 at 22:07)
• restrict linear equiv to submodules (9 messages, latest: Dec 15 2021 at 15:55)
• prod.tendsto_iff (6 messages, latest: Dec 15 2021 at 09:08)
• order_iso for ennreal rpow (16 messages, latest: Dec 14 2021 at 23:03)
• finset.subsingleton (1 message, latest: Dec 14 2021 at 18:01)
• non finsupp finsupp.dom_congr (4 messages, latest: Dec 14 2021 at 11:19)
• ✔ linear_map.to_span_singleton as an equiv (3 messages, latest: Dec 14 2021 at 10:29)
• ✔ Add group structure on localization (18 messages, latest: Dec 12 2021 at 17:09)
• Equivalent of nat.find for positive integers? (26 messages, latest: Dec 12 2021 at 12:52)
• strict mono f on well-order → x ≤ f x (6 messages, latest: Dec 12 2021 at 03:24)
• imp_trans (8 messages, latest: Dec 12 2021 at 00:59)
• Units of product of topological rings (6 messages, latest: Dec 11 2021 at 18:19)
• equal of le and not lt (7 messages, latest: Dec 11 2021 at 13:49)
• Indexed equality (2 messages, latest: Dec 10 2021 at 18:00)
• order on | (3 messages, latest: Dec 10 2021 at 10:55)
• Big-Oh notation (5 messages, latest: Dec 10 2021 at 10:52)
• Local homeomorphisms (5 messages, latest: Dec 10 2021 at 07:37)
• ✔ Disjoint Union of Graphs, or type overrides (12 messages, latest: Dec 09 2021 at 22:06)
• Disjoint Union of Graphs, or type overrides (1 message, latest: Dec 09 2021 at 20:53)
• polynomial.to_finsupp_iso_linear (2 messages, latest: Dec 08 2021 at 14:37)
• adjoin_eq_Inf (14 messages, latest: Dec 08 2021 at 12:20)
• list.fin_range_succ (10 messages, latest: Dec 07 2021 at 14:14)
• Pointwise set division (6 messages, latest: Dec 07 2021 at 14:10)
• Pointwise topology (12 messages, latest: Dec 07 2021 at 13:57)
• ennreal.frontier_Iic (24 messages, latest: Dec 07 2021 at 08:21)
• Addition of interiors (11 messages, latest: Dec 05 2021 at 12:47)
• ✔ Direct product of posets (4 messages, latest: Dec 04 2021 at 04:25)
• Direct product of posets (5 messages, latest: Dec 04 2021 at 04:14)
• push_cast (14 messages, latest: Dec 02 2021 at 14:30)
• rational power (6 messages, latest: Dec 02 2021 at 12:25)
• ennreal.to_nnreal_le_to_nnreal (4 messages, latest: Nov 30 2021 at 18:32)
• Finite geometric sums (10 messages, latest: Nov 30 2021 at 17:51)
• Additive coercions (9 messages, latest: Nov 29 2021 at 22:22)
• integral translation (4 messages, latest: Nov 29 2021 at 15:39)
• lt add (5 messages, latest: Nov 29 2021 at 12:44)
• interior and ord_connected (4 messages, latest: Nov 28 2021 at 20:22)
• Interior of a set-level (5 messages, latest: Nov 28 2021 at 18:51)
• Order on α ⊕ β (16 messages, latest: Nov 27 2021 at 09:07)
• Smoothness of projection from pi (6 messages, latest: Nov 26 2021 at 21:33)
• Subgroup of topological group (3 messages, latest: Nov 26 2021 at 09:35)
• Conditionally complete lattice (32 messages, latest: Nov 26 2021 at 05:15)
• whiskering adjunctions (2 messages, latest: Nov 26 2021 at 04:52)
• order_of (-1) (17 messages, latest: Nov 25 2021 at 07:51)
• evaluation is right adjoint (3 messages, latest: Nov 24 2021 at 21:42)
• order_iso.map_supr (22 messages, latest: Nov 24 2021 at 15:44)
• Localization of localization (5 messages, latest: Nov 24 2021 at 14:51)
• tactic.trace (7 messages, latest: Nov 24 2021 at 13:09)
• Reindexing a dependent product (16 messages, latest: Nov 24 2021 at 12:01)
• ✔ Product of submonoid in commutative monoid (2 messages, latest: Nov 24 2021 at 09:32)
• Product of submonoid in commutative monoid (8 messages, latest: Nov 24 2021 at 09:10)
• Covering relation (4 messages, latest: Nov 23 2021 at 09:24)
• Convergent implies bounded (13 messages, latest: Nov 23 2021 at 07:36)
• Is there a code for extracting square root? (5 messages, latest: Nov 22 2021 at 17:57)
• Is there code to apply ring in an equation (19 messages, latest: Nov 22 2021 at 17:44)
• characteristic two (1 message, latest: Nov 22 2021 at 16:28)
• Continuity of multilinear maps in finite dimensions (6 messages, latest: Nov 19 2021 at 16:17)
• finset.coe_product (5 messages, latest: Nov 19 2021 at 14:01)
• ✔ Trivial fact about multiplication of nats (1 message, latest: Nov 19 2021 at 13:09)
• Trivial fact about multiplication of nats (11 messages, latest: Nov 19 2021 at 12:09)
• (deleted) (2 messages, latest: Nov 19 2021 at 11:24)
• Structure that recurses(?) (9 messages, latest: Nov 18 2021 at 20:03)
• Projection maps (26 messages, latest: Nov 17 2021 at 21:09)
• Probabilistic method (Erdős method) (1 message, latest: Nov 17 2021 at 09:56)
• function.injective fin (32 messages, latest: Nov 15 2021 at 18:34)
• ✔ If s : X.stalk x, it comes from some \(F(V)\) (2 messages, latest: Nov 14 2021 at 01:37)
• If s : X.stalk x, it comes from some \(F(V)\) (6 messages, latest: Nov 13 2021 at 20:58)
• coe to monoid_algebra (9 messages, latest: Nov 13 2021 at 16:34)
• Map eq cons (5 messages, latest: Nov 13 2021 at 12:38)
• Trace of identity (9 messages, latest: Nov 11 2021 at 10:07)
• finset.lcm of positive integers is positive (3 messages, latest: Nov 10 2021 at 23:43)
• Terminal object of cone F (5 messages, latest: Nov 10 2021 at 09:45)
• convex is supremum of affine (13 messages, latest: Nov 08 2021 at 13:54)
• ideal.span_image (12 messages, latest: Nov 08 2021 at 13:34)
• decl_pos and decl_olean for current file (1 message, latest: Nov 08 2021 at 11:25)
• canonical type with 2 terms in universe u (7 messages, latest: Nov 08 2021 at 01:56)
• Prop-valued "I have one term" (21 messages, latest: Nov 07 2021 at 22:50)
• equality in sigma-types (19 messages, latest: Nov 06 2021 at 23:45)
• complex linear and conj linear parts (3 messages, latest: Nov 06 2021 at 18:40)
• sum.inl is an open map (10 messages, latest: Nov 05 2021 at 22:53)
• Product of i < j and j < i (22 messages, latest: Nov 05 2021 at 17:16)
• Cardinality of (fin).filter (19 messages, latest: Nov 05 2021 at 00:22)
• Smoothness of equiv.prod_assoc (26 messages, latest: Nov 04 2021 at 16:39)
• polynomial.eval_prod for multiset (6 messages, latest: Nov 04 2021 at 14:56)
• The kernel of a mapped polynomial is the map of the kernel (6 messages, latest: Nov 04 2021 at 11:40)
• Use "string" instead of "parse texpr" in interactive tactics (2 messages, latest: Nov 04 2021 at 03:08)
• is_iso_ι_of_forall_is_iso (3 messages, latest: Nov 04 2021 at 02:20)
• order isomorphisms preserve disjointness (32 messages, latest: Nov 03 2021 at 21:24)
• filter nones (6 messages, latest: Nov 03 2021 at 21:06)
• homeomorphism between a normed space and a ball (3 messages, latest: Nov 03 2021 at 04:48)
• graded rings (86 messages, latest: Nov 02 2021 at 22:58)
• 4th isomorphism theorem (7 messages, latest: Nov 02 2021 at 18:22)
• Duplicated pow lemmas (3 messages, latest: Nov 02 2021 at 17:16)
• Differentiable from deriv ≠ 0 (2 messages, latest: Nov 02 2021 at 14:42)
• quot.exact given equivalence (7 messages, latest: Nov 02 2021 at 11:22)
• fin_cases on variables (19 messages, latest: Nov 01 2021 at 18:42)
• Smoothness of linear evaluation map (5 messages, latest: Nov 01 2021 at 13:42)
• Perfect matching (2 messages, latest: Oct 30 2021 at 18:59)
• mul_inv_rev for ring_hom.inverse (19 messages, latest: Oct 29 2021 at 18:26)
• ring.inverse equals has_inv.inv (3 messages, latest: Oct 29 2021 at 13:28)
• finset to list (29 messages, latest: Oct 28 2021 at 17:14)
• intermediate_field.adjoin_splits (2 messages, latest: Oct 27 2021 at 22:05)
• Python <-> Lean (6 messages, latest: Oct 27 2021 at 20:31)
• alg_hom from intermediate_field le (8 messages, latest: Oct 27 2021 at 14:57)
• Ico_succ_left_eq_erase_Ico (7 messages, latest: Oct 27 2021 at 12:28)
• counting function (417 messages, latest: Oct 27 2021 at 07:11)
• Multiset subset decidability (1 message, latest: Oct 26 2021 at 12:27)
• modus tollens in context (6 messages, latest: Oct 26 2021 at 06:30)
• A bdd_above set of finsets is finite (18 messages, latest: Oct 25 2021 at 19:28)
• ✔ ring homomorphism commuting with direct sum inclusion (2 messages, latest: Oct 25 2021 at 17:18)
• ring homomorphism commuting with direct sum inclusion (4 messages, latest: Oct 25 2021 at 17:15)
• Passing coe through a sum (3 messages, latest: Oct 24 2021 at 04:58)
• ite.intro (8 messages, latest: Oct 23 2021 at 22:29)
• Search engine (11 messages, latest: Oct 23 2021 at 01:48)
• list.blend (6 messages, latest: Oct 23 2021 at 01:47)
• ✔ equal prime powers (1 message, latest: Oct 22 2021 at 21:29)
• Preconnection in sigma (26 messages, latest: Oct 22 2021 at 14:25)
• Wedderburn's little theorem (18 messages, latest: Oct 22 2021 at 12:20)
• equal prime powers (20 messages, latest: Oct 21 2021 at 19:53)
• ✔ Should linearith be able to solve this? (1 message, latest: Oct 21 2021 at 10:28)
• Should linearith be able to solve this? (6 messages, latest: Oct 21 2021 at 07:43)
• Kuratowski's theorem (3 messages, latest: Oct 20 2021 at 21:42)
• Preterms/Terms, Preformulas/Formulas (9 messages, latest: Oct 20 2021 at 15:00)
• Cardinality of subgroup (38 messages, latest: Oct 20 2021 at 14:32)
• linear_map_bound_of_ball_bound (13 messages, latest: Oct 20 2021 at 14:31)
• Lattice (module) (8 messages, latest: Oct 20 2021 at 07:06)
• ✔ dimension of direct sum (16 messages, latest: Oct 19 2021 at 14:08)
• Choose multiples outside of an ideal (3 messages, latest: Oct 18 2021 at 18:01)
• decompose conjuction/existence chain (4 messages, latest: Oct 17 2021 at 15:01)
• inversion (10 messages, latest: Oct 17 2021 at 01:54)
• Dirichlet's theorem on arithmetic progressions? (23 messages, latest: Oct 16 2021 at 23:45)
• Integral of complex functions (5 messages, latest: Oct 16 2021 at 20:22)
• Affine independent finset (2 messages, latest: Oct 16 2021 at 20:10)
• uniform convergence on a compact set (3 messages, latest: Oct 15 2021 at 19:08)
• Simple algebra / ring (46 messages, latest: Oct 15 2021 at 17:45)
• finset.sup_attach (7 messages, latest: Oct 15 2021 at 08:36)
• Linear basis from spanning set (15 messages, latest: Oct 14 2021 at 19:47)
• Inf and Sup of smul of a set (39 messages, latest: Oct 14 2021 at 08:33)
• set_like disjoint (2 messages, latest: Oct 13 2021 at 19:08)
• The nonnegative elements (17 messages, latest: Oct 13 2021 at 14:06)
• ✔ Cardinality of subtype as a sum (7 messages, latest: Oct 13 2021 at 12:17)
• Cardinality of subtype as a sum (3 messages, latest: Oct 13 2021 at 00:28)
• Things for which there was no documentation i could find (97 messages, latest: Oct 12 2021 at 20:54)
• Cantor_Bernstein (16 messages, latest: Oct 12 2021 at 16:17)
• fintype_of_fintype_ne (29 messages, latest: Oct 12 2021 at 14:18)
• strict_mono_subseq (4 messages, latest: Oct 12 2021 at 13:25)
• [Definitional lemmas for ⟪, ⟫ℂ](topic/Definitional.20lemmas.20for.20.E2.9F.AA.2C.20.E2.9F.AB.E2.84.82.html) (12 messages, latest: Oct 11 2021 at 20:43)
• Direct sum on fintype (5 messages, latest: Oct 11 2021 at 17:43)
• ✔ mapping a fintype into a finset (4 messages, latest: Oct 11 2021 at 08:07)
• finset.drop_none (13 messages, latest: Oct 10 2021 at 16:23)
• ✔ group to group_with_zero (2 messages, latest: Oct 09 2021 at 22:13)
• group to group_with_zero (2 messages, latest: Oct 09 2021 at 22:10)
• modus ponens in context (23 messages, latest: Oct 09 2021 at 17:46)
• le_mul_of_one_le_of_le' for reals (6 messages, latest: Oct 08 2021 at 21:10)
• finset.extend_by_zero variant (25 messages, latest: Oct 08 2021 at 14:50)
• Provability logics (1 message, latest: Oct 08 2021 at 13:32)
• ✔ nat.log is monotonically decreasing on its first argument (3 messages, latest: Oct 08 2021 at 10:15)
• category of objects with distinguished endomorphism (7 messages, latest: Oct 06 2021 at 21:16)
• two_le_add_inv (8 messages, latest: Oct 05 2021 at 15:56)
• smul_pos (3 messages, latest: Oct 05 2021 at 08:10)
• Infinite series is summable iff 'tail' of series is summable (4 messages, latest: Oct 04 2021 at 21:00)
• ✔ Matrix automation??? (6 messages, latest: Oct 04 2021 at 16:28)
• Matrix automation??? (5 messages, latest: Oct 04 2021 at 16:11)
• Convergence of a complex series bounded by a geometric sum (7 messages, latest: Oct 04 2021 at 12:37)
• nat.log is monotonically decreasing on its first argument (21 messages, latest: Oct 04 2021 at 10:23)
• not_def (4 messages, latest: Oct 03 2021 at 20:55)
• nonempty_of_nonempty_subtype (3 messages, latest: Oct 03 2021 at 15:47)
• order_iso.map_cInf (3 messages, latest: Oct 03 2021 at 08:30)
• (lean 4) witness from (decide p && .. && decide n) (18 messages, latest: Sep 30 2021 at 21:35)
• ✔ supr over units ℤ (2 messages, latest: Sep 30 2021 at 14:32)
• Expression printed as AST (5 messages, latest: Sep 30 2021 at 14:05)
• supr over units ℤ (8 messages, latest: Sep 30 2021 at 12:47)
• extract sublist from list (6 messages, latest: Sep 29 2021 at 08:52)
• no injective function on ordinal (2 messages, latest: Sep 28 2021 at 13:26)
• equiv.symm_trans_rev (3 messages, latest: Sep 28 2021 at 10:49)
• sum.elim on function operations (4 messages, latest: Sep 28 2021 at 07:18)
• value multiplied by a unit is associated (6 messages, latest: Sep 27 2021 at 12:28)
• pi_eq_sum_univ for finsupp (28 messages, latest: Sep 25 2021 at 20:50)
• Grid adjacency graph (9 messages, latest: Sep 24 2021 at 19:00)
• ite_eq_imp_iff (6 messages, latest: Sep 24 2021 at 18:33)
• Restricting domains of functions (9 messages, latest: Sep 24 2021 at 18:06)
• inf_Sup_right (28 messages, latest: Sep 24 2021 at 15:04)
• normed space real of complex (11 messages, latest: Sep 24 2021 at 13:41)
• is_zero_object (4 messages, latest: Sep 23 2021 at 17:51)
• mapping a fintype into a finset (12 messages, latest: Sep 23 2021 at 12:20)
• prime_or_zero for naturals (10 messages, latest: Sep 21 2021 at 18:59)
• cases matching with (10 messages, latest: Sep 21 2021 at 09:45)
• Continuity on basic opens (9 messages, latest: Sep 20 2021 at 23:33)
• succ-free induction on nat (3 messages, latest: Sep 20 2021 at 17:44)
• ✔ Rings of char p are a zmod p algebra (5 messages, latest: Sep 19 2021 at 11:47)
• Field of Fractions (4 messages, latest: Sep 18 2021 at 18:24)
• Diagonalization of symmetric matrices (3 messages, latest: Sep 18 2021 at 17:10)
• finset.center_mass as a linear map (4 messages, latest: Sep 17 2021 at 17:47)
• ✔ Change of basis (4 messages, latest: Sep 17 2021 at 11:37)
• x^p is concave for 0 <= p <= 1 (13 messages, latest: Sep 17 2021 at 10:47)
• Gluing of [continuous] functions (21 messages, latest: Sep 17 2021 at 05:13)
• add_lt_of_lt_sub (9 messages, latest: Sep 16 2021 at 22:00)
• maximum of a function (5 messages, latest: Sep 16 2021 at 20:38)
• Selecting element from finite type (21 messages, latest: Sep 16 2021 at 16:21)
• eval2 for alg_homs (3 messages, latest: Sep 14 2021 at 19:16)
• specializing forall to a set (6 messages, latest: Sep 14 2021 at 10:44)
• Polynomial from coefficients (10 messages, latest: Sep 11 2021 at 15:11)
• ✔ differentiation on mv_polynomial (5 messages, latest: Sep 11 2021 at 13:29)
• total_on (3 messages, latest: Sep 11 2021 at 10:54)
• Standard inclusion R^n → R^{n+1} (32 messages, latest: Sep 10 2021 at 15:36)
• Generate explanation for expressions (11 messages, latest: Sep 10 2021 at 09:12)
• ✔ Burnside's Lemma & Polya theorem (1 message, latest: Sep 10 2021 at 07:53)
• ✔ Perron-Frobenius Theorem, Cauchy's Interlacing Theorem? (1 message, latest: Sep 10 2021 at 07:53)
• differentiation on mv_polynomial (6 messages, latest: Sep 10 2021 at 05:01)
• Perron-Frobenius Theorem, Cauchy's Interlacing Theorem? (6 messages, latest: Sep 10 2021 at 04:56)
• Burnside's Lemma & Polya theorem (8 messages, latest: Sep 10 2021 at 04:23)
• Units and Jacobson radical (2 messages, latest: Sep 09 2021 at 22:10)
• ✔ Universal Property of finsupp (5 messages, latest: Sep 09 2021 at 15:50)
• ✔ Basis of matrices (1 message, latest: Sep 09 2021 at 14:43)
• trivial group quotient (12 messages, latest: Sep 09 2021 at 10:52)
• Maximal elements of a partial order (8 messages, latest: Sep 08 2021 at 18:55)
• ✔ integral Union (2 messages, latest: Sep 08 2021 at 17:20)
• subsingleton (set A) of is_empty A (12 messages, latest: Sep 08 2021 at 13:43)
• inequality of prod constructor (12 messages, latest: Sep 08 2021 at 13:15)
• nonzero thing in with_zero X (7 messages, latest: Sep 07 2021 at 20:48)
• Basis of matrices (4 messages, latest: Sep 07 2021 at 15:40)
• integral Union (1 message, latest: Sep 07 2021 at 14:52)
• Chicken Mcnugget/Frobenius coin (13 messages, latest: Sep 06 2021 at 23:45)
• ✔ Vector heq (4 messages, latest: Sep 06 2021 at 22:32)
• viewing an expanded term (10 messages, latest: Sep 06 2021 at 20:44)
• map out of algebra.adjoin (9 messages, latest: Sep 06 2021 at 16:36)
• imp_iff_imp_left (2 messages, latest: Sep 06 2021 at 14:14)
• funext for inequalities (45 messages, latest: Sep 06 2021 at 07:36)
• complete_linear_ordered_add_comm_monoid (9 messages, latest: Sep 06 2021 at 06:46)
• Defining function on union (15 messages, latest: Sep 05 2021 at 21:22)
• Vector heq (1 message, latest: Sep 05 2021 at 21:10)
• has_fderiv.mul in normed algebras ? (4 messages, latest: Sep 05 2021 at 21:00)
• polynomial/finsupp.update (3 messages, latest: Sep 05 2021 at 19:33)
• Directed union of subobject (3 messages, latest: Sep 05 2021 at 14:30)
• pi boolean algebra (6 messages, latest: Sep 05 2021 at 11:29)
• AM-GM (6 messages, latest: Sep 04 2021 at 14:51)
• Vandermonde's identity (9 messages, latest: Sep 04 2021 at 06:38)
• mem_iff for subsingletons (2 messages, latest: Sep 03 2021 at 23:26)
• pointwise min and max (13 messages, latest: Sep 02 2021 at 17:14)
• Sandwich product of vectors and matrices (3 messages, latest: Sep 02 2021 at 10:31)
• linear map from bilinear (8 messages, latest: Sep 02 2021 at 09:32)
• Dependent left_inverse (4 messages, latest: Sep 01 2021 at 11:22)
• Create a blueprint (25 messages, latest: Sep 01 2021 at 10:27)
• index of subgroup (8 messages, latest: Sep 01 2021 at 06:42)
• group acting on algebra (23 messages, latest: Aug 31 2021 at 19:40)
• ordered_module ℚ ℝ (2 messages, latest: Aug 30 2021 at 23:31)
• submodule.supr_mul (17 messages, latest: Aug 30 2021 at 22:27)
• Enumerating a finite subset (28 messages, latest: Aug 30 2021 at 13:10)
• Choosing a finset of minimum cardinality (22 messages, latest: Aug 28 2021 at 07:50)
• monoid_hom for units (13 messages, latest: Aug 27 2021 at 06:17)
• ✔ tactic for structural equality (4 messages, latest: Aug 26 2021 at 09:52)
• prod_dite_of_true (38 messages, latest: Aug 25 2021 at 18:54)
• dependent functions out of a sum equivalent to … (4 messages, latest: Aug 25 2021 at 03:44)
• Hartog's theorem (9 messages, latest: Aug 23 2021 at 23:07)
• coprod and prod on submodules (15 messages, latest: Aug 23 2021 at 19:45)
• Behaviour of finrank under morphisms (32 messages, latest: Aug 22 2021 at 22:36)
• Equivalence class of a setoid (5 messages, latest: Aug 22 2021 at 22:17)
• real.cos is positive iff it is within a union of intervals (2 messages, latest: Aug 21 2021 at 19:18)
• constant if fderiv is zero on connected open sets (1 message, latest: Aug 21 2021 at 06:54)
• ✔ Eventually vacuously true statements (1 message, latest: Aug 19 2021 at 21:32)
• ✔ derivative of (f x⁻¹) (1 message, latest: Aug 19 2021 at 21:32)
• ✔ Asymptotics conversions from equivalents (1 message, latest: Aug 19 2021 at 21:32)
• Totally ordered subsets of a partial order (7 messages, latest: Aug 19 2021 at 20:54)
• ✔ Conjugate of a subgroup (7 messages, latest: Aug 19 2021 at 17:21)
• Asymptotics conversions from equivalents (31 messages, latest: Aug 18 2021 at 23:49)
• Eventually vacuously true statements (4 messages, latest: Aug 18 2021 at 17:11)
• finprod of constant func (9 messages, latest: Aug 18 2021 at 14:53)
• derivative of (f x⁻¹) (4 messages, latest: Aug 18 2021 at 12:59)
• nat.smul_one_eq_coe for enat (3 messages, latest: Aug 18 2021 at 12:45)
• Proving cancellation of deriv at non-differentiable points (1 message, latest: Aug 18 2021 at 12:06)
• Divisibility to adic valuation (8 messages, latest: Aug 18 2021 at 11:19)
• Prime dividing a product (3 messages, latest: Aug 18 2021 at 08:16)
• Sigma assoc (3 messages, latest: Aug 18 2021 at 00:37)
• Moving to the limit in equalities (20 messages, latest: Aug 17 2021 at 18:14)
• Euclidean space (3 messages, latest: Aug 16 2021 at 17:24)
• complex vs real limit (28 messages, latest: Aug 15 2021 at 20:34)
• Restricting permutations (17 messages, latest: Aug 15 2021 at 19:20)
• cardinal.lift_sup (11 messages, latest: Aug 15 2021 at 02:01)
• by_contra! (10 messages, latest: Aug 13 2021 at 13:38)
• Nsatz-like tactic (3 messages, latest: Aug 13 2021 at 05:26)
• quot.forall (5 messages, latest: Aug 12 2021 at 23:34)
• real.summable_of_sum_le (6 messages, latest: Aug 11 2021 at 23:43)
• add_rpow_le (3 messages, latest: Aug 11 2021 at 06:26)
• Composition with injective function is an injective operatio (5 messages, latest: Aug 10 2021 at 15:26)
• discrete topology type alias (11 messages, latest: Aug 10 2021 at 13:04)
• Number between integers not an integer (7 messages, latest: Aug 10 2021 at 07:56)
• completion of a ring at an ideal (4 messages, latest: Aug 09 2021 at 20:18)
• Z is discrete (6 messages, latest: Aug 07 2021 at 18:49)
• differential equations (20 messages, latest: Aug 07 2021 at 17:27)
• quotient homeomorphisms (9 messages, latest: Aug 06 2021 at 19:28)
• Weierstrass M-test (12 messages, latest: Aug 06 2021 at 16:16)
• graph, expander graph, cayley graph, … (10 messages, latest: Aug 06 2021 at 14:25)
• One point compactification (26 messages, latest: Aug 05 2021 at 14:44)
• injective scalar actions (14 messages, latest: Aug 05 2021 at 13:16)
• ite or (3 messages, latest: Aug 05 2021 at 13:06)
• equiv for polynomial ring over opposite ring (19 messages, latest: Aug 03 2021 at 20:03)
• cone equiv (7 messages, latest: Aug 03 2021 at 17:28)
• Example in lean (6 messages, latest: Aug 03 2021 at 01:04)
• Continuous empty map (7 messages, latest: Aug 02 2021 at 20:09)
• A submonoid of a cancel_monoid_with_zero also cancels (4 messages, latest: Aug 02 2021 at 15:34)
• Lifting exponent lemma (6 messages, latest: Aug 02 2021 at 14:57)
• Highest prime power dividing a nat? (4 messages, latest: Aug 02 2021 at 09:22)
• Equitable functions (1 message, latest: Aug 01 2021 at 13:38)
• ✔ Clear true tactic (2 messages, latest: Aug 01 2021 at 05:32)
• The submonoid of positive elements (5 messages, latest: Jul 31 2021 at 17:38)
• aargh dfinsupp is constructive (27 messages, latest: Jul 31 2021 at 16:45)
• Hensel's lemma (5 messages, latest: Jul 31 2021 at 13:16)
• saturating addition on the bottom (19 messages, latest: Jul 31 2021 at 10:29)
• factors lemma (30 messages, latest: Jul 30 2021 at 18:36)
• monoid_hom.map_div (4 messages, latest: Jul 29 2021 at 20:30)
• limits as a class? (18 messages, latest: Jul 29 2021 at 16:32)
• monotonicity for sums and products of monotone functions (16 messages, latest: Jul 29 2021 at 15:11)
• Combining functors (4 messages, latest: Jul 28 2021 at 20:27)
• circulant matrix (40 messages, latest: Jul 28 2021 at 17:26)
• Quotient of a ring by a sum of ideals (30 messages, latest: Jul 28 2021 at 09:36)
• multiset.sum (4 messages, latest: Jul 26 2021 at 21:58)
• ✔ Algebra map is injective (7 messages, latest: Jul 25 2021 at 22:42)
• Algebra map is injective (7 messages, latest: Jul 25 2021 at 21:00)
• Sylow subgroups (8 messages, latest: Jul 24 2021 at 16:26)
• bilinear (3 messages, latest: Jul 23 2021 at 12:02)
• finsetoid (13 messages, latest: Jul 23 2021 at 02:39)
• open private (3 messages, latest: Jul 22 2021 at 08:30)
• getting a linear map from a span (13 messages, latest: Jul 22 2021 at 00:11)
• Local expansions of holomorphic functions (35 messages, latest: Jul 21 2021 at 23:38)
• quotient of a group by a subgroup bijects with left cosets (6 messages, latest: Jul 21 2021 at 09:41)
• If f x ≤ f y → x ≤ y, then f is injective (3 messages, latest: Jul 20 2021 at 13:27)
• ✔ monotone limits (1 message, latest: Jul 18 2021 at 14:19)
• ✔ equalities with set differences (1 message, latest: Jul 18 2021 at 14:18)
• ✔ tendsto_induced (1 message, latest: Jul 18 2021 at 14:18)
• Complex Integral of 1/z round the unit circle (30 messages, latest: Jul 17 2021 at 11:04)
• not some implies none (6 messages, latest: Jul 17 2021 at 01:20)
• tendsto_induced (4 messages, latest: Jul 16 2021 at 23:36)
• equalities with set differences (5 messages, latest: Jul 16 2021 at 15:24)
• Lifting lattice structures (2 messages, latest: Jul 16 2021 at 12:25)
• Subsequence of cauchy seq (10 messages, latest: Jul 15 2021 at 23:13)
• Finitely generated algebras, etc (29 messages, latest: Jul 15 2021 at 17:32)
• Different casts from zmod (17 messages, latest: Jul 15 2021 at 09:06)
• Construct finset from set (6 messages, latest: Jul 14 2021 at 16:45)
• Clear true tactic (9 messages, latest: Jul 14 2021 at 11:32)
• submonoid.mem_supr (4 messages, latest: Jul 13 2021 at 19:10)
• lemmas regarding ε > 0 (7 messages, latest: Jul 13 2021 at 15:17)
• polynomial eval_ring_hom and eval_linear_map (6 messages, latest: Jul 12 2021 at 18:12)
• set.finite_mem_finset (3 messages, latest: Jul 12 2021 at 17:18)
• matrix det (15 messages, latest: Jul 11 2021 at 20:05)
• e as limit of (1+1/n)^n (11 messages, latest: Jul 09 2021 at 18:13)
• bex_and (11 messages, latest: Jul 08 2021 at 23:17)
• n < nat.succ m ↔ n ≤ m (7 messages, latest: Jul 08 2021 at 09:11)
• exists_mem_of_ne_empty (5 messages, latest: Jul 07 2021 at 07:03)
• maps_to.restrict_codom (21 messages, latest: Jul 06 2021 at 22:03)
• psd matrices (5 messages, latest: Jul 06 2021 at 04:09)
• Third isomorphism theorem (7 messages, latest: Jul 05 2021 at 14:30)
• compass and straightedge constructions (2 messages, latest: Jul 04 2021 at 19:05)
• Set from finset is finite (5 messages, latest: Jul 04 2021 at 13:30)
• the obvious monadic adjoint (5 messages, latest: Jul 01 2021 at 01:48)
• Congruent triangles (15 messages, latest: Jun 30 2021 at 22:55)
• abs with constant (11 messages, latest: Jun 30 2021 at 17:28)
• The unique ℂ →ₐ\[ℝ\] A given a square root of -1 (28 messages, latest: Jun 29 2021 at 15:49)
• Collecting terms (6 messages, latest: Jun 29 2021 at 13:54)
• a + b - c = a - c + b (3 messages, latest: Jun 29 2021 at 08:47)
• The canonical ℂ →ₐ\[ℝ\] A given a square root of -1 (1 message, latest: Jun 28 2021 at 12:16)
• The linear map to build a pure imaginary number (9 messages, latest: Jun 27 2021 at 21:54)
• connected_space.is_connected_univ (5 messages, latest: Jun 27 2021 at 18:51)
• Existence of Euler Line (5 messages, latest: Jun 25 2021 at 13:35)
• Can I render my Lean as HTML? (9 messages, latest: Jun 25 2021 at 09:19)
• Sum of functions with disjoint supports (2 messages, latest: Jun 24 2021 at 19:58)
• A ≃ (set.univ A) (7 messages, latest: Jun 24 2021 at 13:10)
• intersection of a set and a finset as a finset (7 messages, latest: Jun 23 2021 at 15:42)
• action on a constant is a linear_map (5 messages, latest: Jun 23 2021 at 08:53)
• Homomorphism induced by left composition (11 messages, latest: Jun 23 2021 at 08:48)
• multiset ext nodup (3 messages, latest: Jun 22 2021 at 19:15)
• nat.factorial lemmas (40 messages, latest: Jun 22 2021 at 08:15)
• Factorization algebras (17 messages, latest: Jun 21 2021 at 08:54)
• R[X] is an R-algebra (6 messages, latest: Jun 19 2021 at 13:20)
• Cardinality of union of finsets (4 messages, latest: Jun 18 2021 at 17:22)
• monotone limits (28 messages, latest: Jun 18 2021 at 09:42)
• Homomorphism from the integers descends to \(\mathbb{Z}/n\) (27 messages, latest: Jun 17 2021 at 16:31)
• (ideal.span {d}).quotient is zmod d (5 messages, latest: Jun 17 2021 at 13:36)
• ∈ gmultiples iff divides (6 messages, latest: Jun 17 2021 at 13:09)
• discrete valuation (34 messages, latest: Jun 17 2021 at 13:03)
• arbitrary linear order (4 messages, latest: Jun 16 2021 at 14:15)
• V(I) /\ V(J) = V(I+J) (14 messages, latest: Jun 16 2021 at 02:53)
• Real subX associated to a complex subX (26 messages, latest: Jun 15 2021 at 14:34)
• convex_on of linear_map (3 messages, latest: Jun 14 2021 at 21:17)
• is_closed_prod (4 messages, latest: Jun 12 2021 at 13:15)
• to_module and map_range (9 messages, latest: Jun 12 2021 at 09:51)
• abelian group decomposition (11 messages, latest: Jun 11 2021 at 09:27)
• Localization of categories (12 messages, latest: Jun 10 2021 at 19:12)
• Replace metavariables by appropriate quantifiers (5 messages, latest: Jun 10 2021 at 09:46)
• type class in "forall/exists" (27 messages, latest: Jun 10 2021 at 08:46)
• Status of Cauchy's integral formula (2 messages, latest: Jun 09 2021 at 18:11)
• trivial module, etc (4 messages, latest: Jun 09 2021 at 14:26)
• submodule.quotient.mk as a linear map (7 messages, latest: Jun 08 2021 at 12:21)
• linear_independent lemmas (7 messages, latest: Jun 08 2021 at 05:59)
• div_le_div (1 message, latest: Jun 07 2021 at 18:03)
• Converse of linear_equiv.congr_arg (9 messages, latest: Jun 07 2021 at 15:09)
• Getting the first element of a nonempty list (6 messages, latest: Jun 07 2021 at 13:02)
• fintype across equiv (12 messages, latest: Jun 06 2021 at 16:52)
• nat_floor (74 messages, latest: Jun 06 2021 at 08:46)
• rpow log exp inequalities (21 messages, latest: Jun 04 2021 at 14:12)
• submodule.le_span (23 messages, latest: Jun 04 2021 at 13:26)
• :golf: (9 messages, latest: Jun 04 2021 at 11:02)
• infi_insert' (1 message, latest: Jun 04 2021 at 10:58)
• homotopy groups of spheres (25 messages, latest: Jun 03 2021 at 19:19)
• Derive is_antisymm (2 messages, latest: Jun 03 2021 at 14:50)
• infinite pigeonhole (4 messages, latest: Jun 03 2021 at 05:35)
• Scalar tower of algebras (4 messages, latest: Jun 02 2021 at 20:30)
• sigma_finsupp_to_dfinsupp (12 messages, latest: Jun 02 2021 at 16:15)
• real sequences: filter.tends_to vs. classical def. (5 messages, latest: Jun 02 2021 at 10:23)
• Multiple cases at once (5 messages, latest: Jun 02 2021 at 09:57)
• topological basis on Inf topology (18 messages, latest: May 31 2021 at 22:10)
• maximal linear independent set? (11 messages, latest: May 31 2021 at 11:40)
• Transferring Instances along Equivs (22 messages, latest: May 31 2021 at 05:04)
• Induced map on homs (4 messages, latest: May 30 2021 at 10:39)
• gsmul API (7 messages, latest: May 30 2021 at 07:12)
• The simplex category (11 messages, latest: May 29 2021 at 22:17)
• Do we have CW complexes? (50 messages, latest: May 29 2021 at 19:55)
• pass between 𝟙 and ring_hom.id (4 messages, latest: May 29 2021 at 12:54)
• not independent of mem span (2 messages, latest: May 29 2021 at 07:07)
• fintype α ⊕ β → fintype α (16 messages, latest: May 28 2021 at 12:56)
• Image of function as finset (9 messages, latest: May 27 2021 at 19:25)
• Kernel of product morphism (18 messages, latest: May 27 2021 at 13:09)
• nnreal.le_div_iff (9 messages, latest: May 26 2021 at 17:58)
• is_compact.nonempty_inter_of… (5 messages, latest: May 26 2021 at 14:55)
• units Rᵒᵖ and (units R)ᵒᵖ are equivalent (2 messages, latest: May 26 2021 at 14:40)
• has_pow (9 messages, latest: May 26 2021 at 14:35)
• Riemann zeta function (8 messages, latest: May 26 2021 at 10:59)
• continuity of coe_fn : C(α, β) → (α → β) (4 messages, latest: May 26 2021 at 10:30)
• functor.eval (7 messages, latest: May 26 2021 at 10:04)
• topology eq of homeomorph (3 messages, latest: May 25 2021 at 12:23)
• Jacobi determinant of f? (2 messages, latest: May 22 2021 at 17:22)
• what sort of lattice is needed? (9 messages, latest: May 22 2021 at 07:23)
• extension of scalars for a module, complexification (10 messages, latest: May 21 2021 at 16:02)
• direct sums of submodules (16 messages, latest: May 21 2021 at 09:31)
• submodule of a submodule (4 messages, latest: May 21 2021 at 08:15)
• Sup in nat belongs to set (22 messages, latest: May 21 2021 at 05:43)
• Disjoint union of totally disconnected spaces (7 messages, latest: May 20 2021 at 16:56)
• surjective endomorphism of a noetherian module is injective? (11 messages, latest: May 20 2021 at 02:42)
• Cantor–Zassenhaus or Berlekamp's algorithm (1 message, latest: May 18 2021 at 17:59)
• Complex analysis - order of vanishing (1 message, latest: May 18 2021 at 14:16)
• Propositions on rational integers (3 messages, latest: May 17 2021 at 20:28)
• Subtypes of functions are equivalent to functions to subtype (2 messages, latest: May 17 2021 at 14:00)
• Countability of eventually identity sequences (2 messages, latest: May 17 2021 at 07:32)
• switching between % and | (6 messages, latest: May 17 2021 at 07:17)
• primes in nat and int (7 messages, latest: May 15 2021 at 12:00)
• list.iterate (4 messages, latest: May 13 2021 at 22:10)
• n-ary zip_with (10 messages, latest: May 13 2021 at 19:58)
• unique from empty (42 messages, latest: May 13 2021 at 05:45)
• exact without definitional unfolding (5 messages, latest: May 11 2021 at 18:54)
• Rank of a vector space (18 messages, latest: May 11 2021 at 09:03)
• monotone coercion (65 messages, latest: May 10 2021 at 16:33)
• image of finset in set (4 messages, latest: May 09 2021 at 23:31)
• split_if1 (2 messages, latest: May 09 2021 at 07:53)
• Exists unique in list (7 messages, latest: May 09 2021 at 04:30)
• Localization at units (46 messages, latest: May 08 2021 at 17:23)
• Switch current goal based on pattern (5 messages, latest: May 07 2021 at 13:59)
• pairwise implying R a b (3 messages, latest: May 07 2021 at 00:51)
• integers are closed in reals (18 messages, latest: May 06 2021 at 22:59)
• modules over a ring (35 messages, latest: May 06 2021 at 09:05)
• Splitting product-like hypotheses (3 messages, latest: May 06 2021 at 01:33)
• Absurd patterns (5 messages, latest: May 05 2021 at 17:30)
• Scalar multiplication by reals is continuous (4 messages, latest: May 05 2021 at 16:45)
• has_coe or id (3 messages, latest: May 05 2021 at 09:30)
• set to finset equiv (15 messages, latest: May 05 2021 at 06:28)
• Infimum of equivalence relations is an equivalence relation (7 messages, latest: May 04 2021 at 18:56)
• submodule span of a subset is finite linear combinations (30 messages, latest: May 04 2021 at 12:20)
• perm of prod is prod of perm (8 messages, latest: May 03 2021 at 14:33)
• finsum over product of types (88 messages, latest: May 02 2021 at 13:26)
• ℝ_p and ℂ_p (3 messages, latest: May 02 2021 at 09:21)
• continuous.sum (9 messages, latest: Apr 30 2021 at 21:28)
• fintype of surjective (5 messages, latest: Apr 30 2021 at 16:35)
• Lattice Homomorphisms? (20 messages, latest: Apr 30 2021 at 14:50)
• equivalence class (1 message, latest: Apr 30 2021 at 14:00)
• left_cancel_semigroup ℝ (11 messages, latest: Apr 30 2021 at 08:06)
• multiplicative.of_add commutes with summation (1 message, latest: Apr 29 2021 at 16:23)
• int.div_eq_zero (5 messages, latest: Apr 28 2021 at 12:53)
• composition of locally constant maps (4 messages, latest: Apr 28 2021 at 04:54)
• ring tactics for characteristic p? (79 messages, latest: Apr 27 2021 at 18:28)
• finset.sum over fin (n+1) (4 messages, latest: Apr 26 2021 at 01:02)
• Birthday Problem (50 messages, latest: Apr 25 2021 at 15:04)
• simplify dite (5 messages, latest: Apr 25 2021 at 03:09)
• Product in over X vs fibered product (12 messages, latest: Apr 24 2021 at 14:44)
• findim_eq_one_iff (5 messages, latest: Apr 24 2021 at 12:50)
• dfinsupp.to_finsupp (7 messages, latest: Apr 24 2021 at 08:10)
• R^m is finite dimensional over R (45 messages, latest: Apr 23 2021 at 17:31)
• has_inv.inv as a monoid_hom on groups (7 messages, latest: Apr 22 2021 at 17:51)
• searching by type (5 messages, latest: Apr 22 2021 at 09:30)
• cardinality of disjoint union (8 messages, latest: Apr 21 2021 at 17:09)
• finsupp equiv dfinsupp (2 messages, latest: Apr 20 2021 at 23:20)
• convex hull of an insert (3 messages, latest: Apr 20 2021 at 13:38)
• left/right unification (11 messages, latest: Apr 20 2021 at 12:53)
• modular forms and Hecke operators (7 messages, latest: Apr 19 2021 at 09:07)
• dist on real (3 messages, latest: Apr 18 2021 at 12:13)
• smul_const for filters (9 messages, latest: Apr 17 2021 at 23:25)
• rational functions (17 messages, latest: Apr 17 2021 at 20:28)
• convex hulls and compact convex sets (30 messages, latest: Apr 17 2021 at 19:34)
• Minkowski Lattice Theorem (7 messages, latest: Apr 17 2021 at 06:35)
• diagram chase thingy (7 messages, latest: Apr 16 2021 at 22:10)
• continuous_on.dif (13 messages, latest: Apr 15 2021 at 21:18)
• Scaling of open set is open (11 messages, latest: Apr 15 2021 at 17:42)
• Linear map is continuous if it's continuous at zero (9 messages, latest: Apr 15 2021 at 16:59)
• positive reals (18 messages, latest: Apr 15 2021 at 07:47)
• Additive/Multiplicative closure (10 messages, latest: Apr 15 2021 at 07:40)
• max over compact of continuous (7 messages, latest: Apr 15 2021 at 07:35)
• direct_sum.to_add_monoid_apply (14 messages, latest: Apr 14 2021 at 21:39)
• by symmetry (28 messages, latest: Apr 14 2021 at 08:40)
• Inf of scalar product (3 messages, latest: Apr 13 2021 at 22:50)
• finset.sup' (51 messages, latest: Apr 13 2021 at 07:44)
• Barycentric coordinates (7 messages, latest: Apr 12 2021 at 22:23)
• For naturals m < m', there is a positive integer s.th…. (12 messages, latest: Apr 12 2021 at 20:08)
• Graphs and paths in graphs (40 messages, latest: Apr 11 2021 at 03:05)
• Functorial version of obj (5 messages, latest: Apr 10 2021 at 23:36)
• order dot final (2 messages, latest: Apr 10 2021 at 16:39)
• mul_right_comm_monoid (2 messages, latest: Apr 10 2021 at 00:05)
• total preorder to linear order (18 messages, latest: Apr 09 2021 at 20:50)
• set membership (4 messages, latest: Apr 09 2021 at 20:20)
• fintype.equiv_fin + fin.cast (29 messages, latest: Apr 09 2021 at 16:19)
• tangent bundle is a topological_vector_bundle (10 messages, latest: Apr 09 2021 at 09:00)
• iterate.comm (73 messages, latest: Apr 09 2021 at 07:02)
• exists simplifying ors (3 messages, latest: Apr 08 2021 at 07:31)
• negation of funext? (8 messages, latest: Apr 07 2021 at 14:03)
• Powers of a relation? (8 messages, latest: Apr 07 2021 at 01:57)
• Root Exports (15 messages, latest: Apr 06 2021 at 20:59)
• Ascending chain conditions (38 messages, latest: Apr 06 2021 at 20:07)
• is_closed.graph (12 messages, latest: Apr 06 2021 at 15:02)
• Symmetric matrix eigen-decomposition (7 messages, latest: Apr 06 2021 at 11:58)
• Homeomorphisms between [0,1] and [a,b]? (4 messages, latest: Apr 06 2021 at 08:09)
• equiv.set renamed? (3 messages, latest: Apr 06 2021 at 07:07)
• finset.subset_iff_inter_eq_left / right (14 messages, latest: Apr 06 2021 at 05:31)
• fintype.of_finset alternative (4 messages, latest: Apr 05 2021 at 23:24)
• Eventually monotone sequences converge (7 messages, latest: Apr 05 2021 at 22:42)
• set.finite.of_surjective (3 messages, latest: Apr 05 2021 at 22:01)
• continuous.of_locally_constant (9 messages, latest: Apr 05 2021 at 20:07)
• divisor dividend and remained for nat (3 messages, latest: Apr 05 2021 at 16:59)
• product tends to zero (22 messages, latest: Apr 05 2021 at 16:51)
• {0 -> 1} as a category (10 messages, latest: Apr 02 2021 at 18:51)
• Sums over finsets and fintypes (9 messages, latest: Apr 02 2021 at 12:22)
• algebra_map.injective.linear_independent (5 messages, latest: Apr 01 2021 at 18:57)
• transitive group action (14 messages, latest: Apr 01 2021 at 14:32)
• inequality lemma (18 messages, latest: Mar 31 2021 at 23:38)
• pullbacks in Type u (9 messages, latest: Mar 31 2021 at 07:42)
• Urysohn's Lemma? (6 messages, latest: Mar 30 2021 at 21:18)
• has_terminal.of_is_terminal (5 messages, latest: Mar 30 2021 at 20:03)
• Cardinality of quotient ≤ (7 messages, latest: Mar 30 2021 at 18:20)
• Rank of a linear map is lower semi continuous (8 messages, latest: Mar 30 2021 at 05:27)
• axiom of choice for finite collections? (5 messages, latest: Mar 29 2021 at 20:10)
• Transporting mul_action along a monoid_hom (6 messages, latest: Mar 29 2021 at 10:27)
• submodule.quotient.mk as a linear map? (12 messages, latest: Mar 29 2021 at 02:32)
• (-1)^k when k is an int (2 messages, latest: Mar 28 2021 at 12:42)
• nat.log_mono (7 messages, latest: Mar 26 2021 at 20:49)
• better/best solving AI? (39 messages, latest: Mar 26 2021 at 09:09)
• injective.map_swap (4 messages, latest: Mar 25 2021 at 17:15)
• fin.rotate (57 messages, latest: Mar 24 2021 at 17:40)
• gcd_nsmul_eq_zero? (4 messages, latest: Mar 23 2021 at 08:20)
• left_inverse imples ` α ≃ set.range f` (2 messages, latest: Mar 22 2021 at 18:09)
• group_with_zero morphisms with domain ℚ (37 messages, latest: Mar 21 2021 at 21:36)
• nodup vs. count vs length (7 messages, latest: Mar 21 2021 at 00:21)
• Injectivity of field extensions (4 messages, latest: Mar 20 2021 at 20:46)
• frequently_in_nhds_map (24 messages, latest: Mar 20 2021 at 03:46)
• structure theorem for finite boolean algebras (7 messages, latest: Mar 19 2021 at 18:59)
• no_zero_divisors instance on polynomials? (6 messages, latest: Mar 19 2021 at 08:45)
• mul_neg (8 messages, latest: Mar 19 2021 at 06:57)
• Cancelling in a domain (3 messages, latest: Mar 19 2021 at 06:17)
• line_map (4 messages, latest: Mar 19 2021 at 03:36)
• group.div_self (7 messages, latest: Mar 18 2021 at 12:05)
• Projective R-modules. (44 messages, latest: Mar 17 2021 at 23:19)
• algebraic structures on lists (4 messages, latest: Mar 17 2021 at 16:46)
• singleton embedding (4 messages, latest: Mar 17 2021 at 16:42)
• subsingleton from card = 1 (3 messages, latest: Mar 16 2021 at 16:11)
• IMO 2012-4 (3 messages, latest: Mar 16 2021 at 15:14)
• is_square/is_power (29 messages, latest: Mar 16 2021 at 14:44)
• continuous_sup (12 messages, latest: Mar 16 2021 at 10:57)
• sup norm on continuous functions? (31 messages, latest: Mar 16 2021 at 01:03)
• (continous) linear_maps between p and p.restrict_scalars (1 message, latest: Mar 15 2021 at 14:35)
• transport has_limits w.r.t. equivalence (16 messages, latest: Mar 15 2021 at 14:16)
• Products of non-commutative monoids (42 messages, latest: Mar 15 2021 at 07:37)
• Integrals on [0, +inf[ as limits (27 messages, latest: Mar 14 2021 at 22:09)
• break off last term of summation (16 messages, latest: Mar 14 2021 at 16:42)
• Sums and products with multiplicative/additive (3 messages, latest: Mar 14 2021 at 14:59)
• Matrix on edge set for graphs (51 messages, latest: Mar 12 2021 at 19:45)
• finsupp.single (f x) y (f z) = finsupp.single x y z (2 messages, latest: Mar 12 2021 at 16:11)
• poly (a)eval and algebra maps (13 messages, latest: Mar 11 2021 at 19:32)
• Cokers of morphisms of add_comm_groups (5 messages, latest: Mar 11 2021 at 07:30)
• succ_succ_ne_one (27 messages, latest: Mar 11 2021 at 06:13)
• Correct setting for positive shifts of intervals (37 messages, latest: Mar 10 2021 at 20:27)
• list.update_nth_same (9 messages, latest: Mar 10 2021 at 13:49)
• le on option (5 messages, latest: Mar 09 2021 at 19:30)
• Bilinear form on finsupp (6 messages, latest: Mar 09 2021 at 18:25)
• Reduce like operation for finite sets (14 messages, latest: Mar 08 2021 at 22:58)
• add_sub_swap (5 messages, latest: Mar 08 2021 at 12:28)
• generators smul generators generate (76 messages, latest: Mar 07 2021 at 15:08)
• affine span is convex (6 messages, latest: Mar 06 2021 at 23:20)
• G-module maps (20 messages, latest: Mar 06 2021 at 20:03)
• Sum is linear (19 messages, latest: Mar 06 2021 at 18:53)
• list.update_same (2 messages, latest: Mar 04 2021 at 13:47)
• le_or_le (7 messages, latest: Mar 04 2021 at 07:55)
• functor.comp as a functor (3 messages, latest: Mar 03 2021 at 21:06)
• Is there a ring instance on a semiring that is a ℤ-alge… (9 messages, latest: Mar 03 2021 at 08:47)
• ne of mem and not mem (12 messages, latest: Mar 03 2021 at 03:47)
• topology without filters (3 messages, latest: Mar 02 2021 at 05:11)
• Category of diagrams (5 messages, latest: Mar 01 2021 at 23:25)
• linear image of segment (5 messages, latest: Mar 01 2021 at 23:09)
• linear map to matrices, ring_equiv (41 messages, latest: Mar 01 2021 at 19:35)
• classicalize (80 messages, latest: Mar 01 2021 at 10:04)
• inequality involving /2 (6 messages, latest: Mar 01 2021 at 07:32)
• "Reversing" fin (10 messages, latest: Feb 28 2021 at 12:25)
• Filter golf (83 messages, latest: Feb 27 2021 at 16:44)
• A strict_mono function from ℕ is determined by its image (3 messages, latest: Feb 27 2021 at 16:22)
• nonempty linear_order (4 messages, latest: Feb 27 2021 at 08:38)
• measure theory for algebraists (8 messages, latest: Feb 26 2021 at 21:56)
• constructing subalgebra without duplicate axioms (2 messages, latest: Feb 25 2021 at 19:40)
• Chauchy-Schwarz (9 messages, latest: Feb 24 2021 at 18:11)
• Transitive symmetric relations (12 messages, latest: Feb 24 2021 at 13:17)
• mem_span_of_mem_span (11 messages, latest: Feb 23 2021 at 13:07)
• well-founded linear order on a type (3 messages, latest: Feb 22 2021 at 22:13)
• Unfolding let bindings in hypotheses (81 messages, latest: Feb 22 2021 at 18:17)
• Finiteness of balls in the integers (5 messages, latest: Feb 22 2021 at 14:28)
• linear maps in the constructor for power_series (6 messages, latest: Feb 22 2021 at 13:34)
• Order from embedding (50 messages, latest: Feb 21 2021 at 17:21)
• Integrals on [0, +inf] as limits (1 message, latest: Feb 20 2021 at 23:10)
• A typeclass for nat subtraction (18 messages, latest: Feb 20 2021 at 18:41)
• int.iterate (8 messages, latest: Feb 20 2021 at 17:10)
• functors and universe constraints (10 messages, latest: Feb 20 2021 at 09:35)
• distinct (14 messages, latest: Feb 19 2021 at 19:31)
• Linear indep of nonzero smul (1 message, latest: Feb 19 2021 at 17:31)
• General lift (5 messages, latest: Feb 19 2021 at 16:51)
• Simple integral calculations (27 messages, latest: Feb 19 2021 at 08:53)
• by_cases foo, {finish} (9 messages, latest: Feb 18 2021 at 22:31)
• nontrivial matrices (6 messages, latest: Feb 18 2021 at 17:13)
• Converting from one type to another (15 messages, latest: Feb 18 2021 at 15:29)
• integral_restrict (20 messages, latest: Feb 18 2021 at 12:53)
• assume h and then prove cases for h and not h (11 messages, latest: Feb 18 2021 at 10:37)
• list.nth is either none (5 messages, latest: Feb 16 2021 at 19:29)
• set.erase (3 messages, latest: Feb 16 2021 at 17:57)
• complement of finite in infinite is infinite (21 messages, latest: Feb 16 2021 at 17:39)
• monotone increasing or decreasing subsequence (11 messages, latest: Feb 16 2021 at 02:59)
• additive functors (8 messages, latest: Feb 16 2021 at 02:01)
• Krull dimension, regular rings (8 messages, latest: Feb 15 2021 at 11:56)
• not_mem lemmas (4 messages, latest: Feb 15 2021 at 06:55)
• Injective map inducing perm group homomorphism (2 messages, latest: Feb 15 2021 at 04:15)
• range with step (7 messages, latest: Feb 14 2021 at 17:54)
• different gcd's? (16 messages, latest: Feb 13 2021 at 01:57)
• linear maps (4 messages, latest: Feb 11 2021 at 11:05)
• Homomorphism estensionnality (7 messages, latest: Feb 11 2021 at 09:39)
• lt_of_add_lt (9 messages, latest: Feb 11 2021 at 08:21)
• First isomorphism theorem for rings (33 messages, latest: Feb 11 2021 at 06:48)
• discrete bot (2 messages, latest: Feb 10 2021 at 21:36)
• fintype_of_univ_finite (2 messages, latest: Feb 10 2021 at 21:36)
• primes associated of dvd (20 messages, latest: Feb 10 2021 at 19:33)
• Special cases of Fermat's Last Theorem (10 messages, latest: Feb 10 2021 at 11:28)
• powers are monotone in the base (6 messages, latest: Feb 10 2021 at 06:42)
• prime generator of prime ideal (3 messages, latest: Feb 09 2021 at 10:19)
• Membership in Sup of submodules (7 messages, latest: Feb 09 2021 at 03:47)
• linear map of subspace ne top (12 messages, latest: Feb 06 2021 at 02:45)
• P-adic valuation on polynomials (21 messages, latest: Feb 05 2021 at 15:41)
• evaluation map from sets to sets (16 messages, latest: Feb 03 2021 at 23:07)
• Halves of a sorted list are related (52 messages, latest: Feb 03 2021 at 19:14)
• lifting sub from Q to N? (6 messages, latest: Feb 03 2021 at 17:45)
• lt on functions (2 messages, latest: Feb 03 2021 at 14:37)
• tsum_lt? (39 messages, latest: Feb 03 2021 at 14:24)
• nat.find_ge_of_not? (5 messages, latest: Feb 03 2021 at 00:04)
• real.log_ne_zero_iff? (25 messages, latest: Feb 02 2021 at 13:23)
• Swapping quotients (2 messages, latest: Feb 02 2021 at 04:35)
• Semifields? (53 messages, latest: Feb 01 2021 at 21:27)
• Quotient thing (7 messages, latest: Feb 01 2021 at 16:28)
• exists_unique from equiv (17 messages, latest: Feb 01 2021 at 12:36)
• induction on n where n ≠ 0 (32 messages, latest: Feb 01 2021 at 06:30)
• int in other universes (9 messages, latest: Jan 31 2021 at 21:41)
• norm as a quadratic form (6 messages, latest: Jan 31 2021 at 18:26)
• saturated submonoids, kernels and beyond (25 messages, latest: Jan 31 2021 at 17:51)
• degree_prod (22 messages, latest: Jan 31 2021 at 07:30)
• condition on type class (5 messages, latest: Jan 30 2021 at 22:42)
• Bezout (12 messages, latest: Jan 30 2021 at 00:56)
• Inverse finset.product (12 messages, latest: Jan 29 2021 at 17:24)
• Get single element from finset (10 messages, latest: Jan 29 2021 at 15:14)
• Is there a definition of a Z-module nZ for any n? (7 messages, latest: Jan 29 2021 at 14:19)
• "classical" definition of limit of sequence (5 messages, latest: Jan 29 2021 at 01:50)
• holomorphic functions on the upper half plane (18 messages, latest: Jan 27 2021 at 15:05)
• Liquid Tensor Experiment (3 messages, latest: Jan 25 2021 at 07:07)
• Bilattices (16 messages, latest: Jan 23 2021 at 17:54)
• finite_dimensional_of_findim_pos (2 messages, latest: Jan 22 2021 at 19:15)
• cardinal.pos_of_one_le (10 messages, latest: Jan 22 2021 at 16:49)
• CW Complex (6 messages, latest: Jan 22 2021 at 11:43)
• matrix.dot_product is a linear map (5 messages, latest: Jan 22 2021 at 09:30)
• Application of add_monoid_hom distributes over sum (3 messages, latest: Jan 22 2021 at 08:50)
• minimal_polynomial_degree_one (3 messages, latest: Jan 22 2021 at 02:57)
• monotonicty of l^p norms (6 messages, latest: Jan 21 2021 at 13:25)
• Indexing with multiset (19 messages, latest: Jan 21 2021 at 00:28)
• even powers (7 messages, latest: Jan 20 2021 at 20:36)
• wikipedia flavored stochastic_process (1 message, latest: Jan 20 2021 at 20:25)
• nat cast is a member of ideal / subring if 1 is (3 messages, latest: Jan 19 2021 at 16:51)
• iff.intro quotient.exact' quotient.sound' (8 messages, latest: Jan 19 2021 at 12:58)
• subset of subset (12 messages, latest: Jan 18 2021 at 21:54)
• can assume n is minimal (6 messages, latest: Jan 18 2021 at 15:36)
• list.update_nth_comm (2 messages, latest: Jan 16 2021 at 22:29)
• A Different finset.fold (5 messages, latest: Jan 16 2021 at 12:10)
• Classical Choice on finset (7 messages, latest: Jan 15 2021 at 21:32)
• Matrix multiplication (4 messages, latest: Jan 15 2021 at 14:28)
• comm_semiring structure on constructible subsets (111 messages, latest: Jan 14 2021 at 20:48)
• structure preserving maps (3 messages, latest: Jan 14 2021 at 15:15)
• monotone right inverse (3 messages, latest: Jan 14 2021 at 12:51)
• class instance in hypothesis (9 messages, latest: Jan 14 2021 at 00:21)
• Zeta functions (27 messages, latest: Jan 13 2021 at 22:16)
• A typeclass for (r : R) (x y : A) : (r • x)*y = r • (x*y) (7 messages, latest: Jan 13 2021 at 18:02)
• Summing over monoid_hom.range (7 messages, latest: Jan 12 2021 at 20:21)
• ite lemma (5 messages, latest: Jan 12 2021 at 19:47)
• Swap List Element (3 messages, latest: Jan 12 2021 at 13:07)
• Bézout's identity (15 messages, latest: Jan 12 2021 at 11:47)
• If an equiv is contained with a set then so is its inverse (7 messages, latest: Jan 12 2021 at 10:44)
• Generic Types (5 messages, latest: Jan 12 2021 at 05:44)
• Flatten Option (24 messages, latest: Jan 11 2021 at 19:10)
• cardinal (11 messages, latest: Jan 11 2021 at 15:45)
• Bicommutant (2 messages, latest: Jan 10 2021 at 04:45)
• Is there code for det (8 messages, latest: Jan 09 2021 at 23:44)
• The closed interval [0,1] (4 messages, latest: Jan 09 2021 at 21:00)
• n = m if fin m ≃ fin n (7 messages, latest: Jan 08 2021 at 20:42)
• a * a ∣ b * b → a ∣ b on the integers (8 messages, latest: Jan 06 2021 at 11:34)
• telescoping sum (5 messages, latest: Jan 05 2021 at 08:37)
• Member of a set is a member of its span (7 messages, latest: Jan 05 2021 at 08:26)
• measure_space.pi (5 messages, latest: Jan 03 2021 at 23:22)
• Simple Subtype (6 messages, latest: Jan 03 2021 at 21:41)
• Maximal ideals are pairwise coprime (5 messages, latest: Jan 03 2021 at 20:03)
• Mapping finset.univ along an equiv gives finset.univ (2 messages, latest: Jan 03 2021 at 18:38)
• API for Z/(n) = zmod n (7 messages, latest: Jan 02 2021 at 06:34)
• Classification of finite-dimensional vector spaces (36 messages, latest: Jan 02 2021 at 06:18)
• Symmetric maps on n variables (3 messages, latest: Jan 01 2021 at 19:02)
• Closure Operators / Matroids (42 messages, latest: Jan 01 2021 at 02:14)
• Function Property for rel (4 messages, latest: Dec 31 2020 at 21:07)
• add_subgroup of normed_group (3 messages, latest: Dec 31 2020 at 20:22)
• injective.ne (63 messages, latest: Dec 31 2020 at 12:01)
• Automorphisms of ℂ (6 messages, latest: Dec 31 2020 at 07:04)
• integer polynomials (4 messages, latest: Dec 29 2020 at 17:23)
• Membership-Proof in filter (2 messages, latest: Dec 28 2020 at 17:13)
• (m+n)!/(m!n!) (45 messages, latest: Dec 28 2020 at 14:46)
• nth_le with different le (3 messages, latest: Dec 26 2020 at 20:50)
• Filtered category equivalence (7 messages, latest: Dec 24 2020 at 15:15)
• ∀ a₁ a₂ : A, f a₁ a₂ = f a₂ a₁ (42 messages, latest: Dec 22 2020 at 21:35)
• columns not linear_independent implies determinant zero (2 messages, latest: Dec 22 2020 at 13:29)
• Split prop into T/F cases (2 messages, latest: Dec 21 2020 at 22:32)
• Characterization of closed subspace (16 messages, latest: Dec 21 2020 at 19:22)
• homeo of induced by equiv (7 messages, latest: Dec 18 2020 at 23:25)
• smul of tmul by ℕ and ℤ (10 messages, latest: Dec 18 2020 at 18:14)
• multiset.filter_count (3 messages, latest: Dec 18 2020 at 12:15)
• intervals, abs and shifts (10 messages, latest: Dec 18 2020 at 09:36)
• work_on_goals (7 messages, latest: Dec 17 2020 at 22:15)
• set with two elements (13 messages, latest: Dec 17 2020 at 02:46)
• metavariable (9 messages, latest: Dec 16 2020 at 22:34)
• Exponential (72 messages, latest: Dec 16 2020 at 21:34)
• disjoint_nhds_finite_of_t2 (130 messages, latest: Dec 16 2020 at 17:29)
• Functor commutes with finite (co)limits (21 messages, latest: Dec 15 2020 at 18:02)
• How can one represent Calculus limits using filters? (20 messages, latest: Dec 15 2020 at 09:42)
• mul_zero_class ℕ (6 messages, latest: Dec 15 2020 at 04:37)
• Partial sums bounded implies summable (17 messages, latest: Dec 14 2020 at 11:10)
• (commutative)-semirng (105 messages, latest: Dec 14 2020 at 09:43)
• completion of boolean algebra (4 messages, latest: Dec 13 2020 at 15:59)
• Induction on lattices (10 messages, latest: Dec 12 2020 at 22:19)
• finset.has_coe_to_sort (9 messages, latest: Dec 12 2020 at 20:54)
• Inner product space is metric space (7 messages, latest: Dec 12 2020 at 20:50)
• semidecidable (26 messages, latest: Dec 12 2020 at 14:52)
• mul_action on quotient_group.quotient (4 messages, latest: Dec 12 2020 at 13:23)
• If it's not sum.inr then it's sum.inr (40 messages, latest: Dec 12 2020 at 12:16)
• Best way to choose five distinct elements from a set? (14 messages, latest: Dec 12 2020 at 09:15)
• extend to set.insert (4 messages, latest: Dec 12 2020 at 08:33)
• range(n,m) (7 messages, latest: Dec 11 2020 at 13:17)
• int_to_expr (1 message, latest: Dec 11 2020 at 13:02)
• interchange sum (40 messages, latest: Dec 11 2020 at 12:05)
• Does mathlib have infinity and a type of extended reals? (14 messages, latest: Dec 11 2020 at 11:57)
• A bounded set of integers is finite (25 messages, latest: Dec 11 2020 at 00:19)
• finset.comap (10 messages, latest: Dec 10 2020 at 21:09)
• An add_monoid_hom is a linear_map ℤ (62 messages, latest: Dec 10 2020 at 13:30)
• compute degree and leading term (8 messages, latest: Dec 09 2020 at 14:56)
• Probability measure of B(R) and B([0,1]) (18 messages, latest: Dec 09 2020 at 02:59)
• continuous implies integrable (16 messages, latest: Dec 09 2020 at 02:42)
• pi_instance for products (7 messages, latest: Dec 09 2020 at 02:24)
• Converting a finset to a list (16 messages, latest: Dec 08 2020 at 17:44)
• Should I be using has_dist vs abbreviation metric (9 messages, latest: Dec 08 2020 at 14:58)
• [The subgroup containing only 1 and x when xx=1](topic/The.20subgroup.20containing.20only.201.20and.20x.20when.20xx.3D1.html) (21 messages, latest: Dec 08 2020 at 07:54)
• quotient.exists_rep without a typeclass instance (17 messages, latest: Dec 07 2020 at 22:13)
• Presheaves have all (co)limits (13 messages, latest: Dec 07 2020 at 17:29)
• Is this a good foundational definition for random variable? (73 messages, latest: Dec 07 2020 at 13:54)
• equiv.perm.sign (equiv.sum_congr σa σb) = σa.sign * σb.sign (4 messages, latest: Dec 07 2020 at 10:07)
• BNF (1 message, latest: Dec 07 2020 at 01:06)
• How do I make a Wikipedia-style metric space in Lean? (183 messages, latest: Dec 07 2020 at 00:23)
• Are [0,1], (0,1), [0,oo) predefined in mathlib.20predefined.20in.20mathlib.html) (12 messages, latest: Dec 06 2020 at 19:04)
• Quotient of a fintype is a fintype (8 messages, latest: Dec 06 2020 at 11:15)
• where is the code for group.to_monoid (2 messages, latest: Dec 06 2020 at 05:10)
• Basis for quotient of polynomial ring (12 messages, latest: Dec 04 2020 at 19:07)
• (he.to_matrix v)ᵀ i = he.repr (v i) (10 messages, latest: Dec 04 2020 at 11:42)
• Image of submodule under linear map (11 messages, latest: Dec 04 2020 at 08:19)
• Algebraic extension of algebraically closed field (7 messages, latest: Dec 04 2020 at 01:58)
• metrics are nonnegative (52 messages, latest: Dec 03 2020 at 23:44)
• (@univ $ perm ι).card = (card ι).factorial (16 messages, latest: Dec 03 2020 at 17:56)
• A vector range (7 messages, latest: Dec 03 2020 at 10:04)
• Splitting(?) an ultrafilter (14 messages, latest: Dec 02 2020 at 23:27)
• finset.sum_surj (19 messages, latest: Dec 02 2020 at 16:49)
• Instances on sum.elim A B i (31 messages, latest: Dec 02 2020 at 14:09)
• The tensor product of two multilinear maps is a multiline… (10 messages, latest: Dec 02 2020 at 09:42)
• The linear map from a b : A, a ⊗ₜ b to a * b (2 messages, latest: Dec 02 2020 at 08:49)
• convex polyhedra (21 messages, latest: Dec 01 2020 at 21:20)
• is this lemma true? (4 messages, latest: Nov 30 2020 at 21:33)
• Simple nat.sqrt lemmas (7 messages, latest: Nov 30 2020 at 20:23)
• integral of piecewise constant function (10 messages, latest: Nov 30 2020 at 16:20)
• [or.elim into Type](topic/or.2Eelim.20into.20Type.html) (5 messages, latest: Nov 29 2020 at 21:05)
• Splitting a finset.sum over an involutive function (13 messages, latest: Nov 28 2020 at 11:30)
• Guessing the structure from the axioms (5 messages, latest: Nov 27 2020 at 19:18)
• eval_zero is a bundled semiring hom (29 messages, latest: Nov 27 2020 at 19:10)
• If f is a multilinear map then λ v, f (v ∘ σ) is too (11 messages, latest: Nov 27 2020 at 18:47)
• gsmul and smul commute (4 messages, latest: Nov 27 2020 at 18:37)
• x.pred < y.pred iff x < y (6 messages, latest: Nov 26 2020 at 16:27)
• sum.elim (f ∘ sum.inl) (f ∘ sum.inr) = f (58 messages, latest: Nov 26 2020 at 15:57)
• name-hunt: Union_of_singleton? (18 messages, latest: Nov 26 2020 at 14:03)
• monad finset (3 messages, latest: Nov 26 2020 at 11:46)
• fin (n + m) → fin n ⊕ fin m (17 messages, latest: Nov 25 2020 at 18:27)
• t2_space instances for disjoint union (5 messages, latest: Nov 25 2020 at 15:31)
• disjoint sets in djsoint union (20 messages, latest: Nov 24 2020 at 22:59)
• Running doc-gen against an external repository (26 messages, latest: Nov 23 2020 at 19:13)
• has_mem for subgroup of units (8 messages, latest: Nov 23 2020 at 16:30)
• normal subgroups (49 messages, latest: Nov 23 2020 at 07:16)
• linear_ordered_comm_group (3 messages, latest: Nov 20 2020 at 20:12)
• Submonoids under which mul_action.smul is closed (66 messages, latest: Nov 20 2020 at 04:21)
• free_abelian_group.of is injective (25 messages, latest: Nov 18 2020 at 13:09)
• algebra R (M →ₗ[R] M) (28 messages, latest: Nov 18 2020 at 12:34)
• ∀ (r : ℝ), ∥r∥^2 = r * r (12 messages, latest: Nov 17 2020 at 14:42)
• Triviality of a quotient group implying subgroup is top (5 messages, latest: Nov 17 2020 at 05:51)
• take pairs (10 messages, latest: Nov 16 2020 at 10:05)
• probability (135 messages, latest: Nov 15 2020 at 15:19)
• Inline type hints (4 messages, latest: Nov 15 2020 at 01:03)
• Distributing prod.fst or prod.snd over an ite (6 messages, latest: Nov 13 2020 at 20:50)
• finite groups? (4 messages, latest: Nov 11 2020 at 19:39)
• Difference between submodules (44 messages, latest: Nov 10 2020 at 14:50)
• set.univ is \top (9 messages, latest: Nov 10 2020 at 14:39)
• two parallel hypotheses in a lemma (27 messages, latest: Nov 10 2020 at 09:15)
• Multiplication of sets (17 messages, latest: Nov 09 2020 at 23:27)
• Monoid hom preserves identity (24 messages, latest: Nov 09 2020 at 15:45)
• totally disconnected of discrete (15 messages, latest: Nov 08 2020 at 19:43)
• Grp is not CCC (40 messages, latest: Nov 06 2020 at 19:03)
• mem.span (191 messages, latest: Nov 04 2020 at 22:52)
• mul_action_hom (9 messages, latest: Nov 03 2020 at 15:46)
• concrete limits in Type (12 messages, latest: Nov 02 2020 at 20:37)
• nat.rec? (12 messages, latest: Oct 31 2020 at 21:22)
• Subset of finset is finset (36 messages, latest: Oct 31 2020 at 16:43)
• Hilbert space is isometric to its dual (77 messages, latest: Oct 30 2020 at 01:25)
• nat.eq_of_fin_equiv (18 messages, latest: Oct 28 2020 at 22:38)
• The category of finite sets (28 messages, latest: Oct 27 2020 at 18:26)
• Surreal numbers (19 messages, latest: Oct 27 2020 at 15:28)
• Simple integer divisibility (8 messages, latest: Oct 27 2020 at 14:53)
• left/right cancelative semiring (64 messages, latest: Oct 27 2020 at 09:51)
• Convexity and products (7 messages, latest: Oct 25 2020 at 22:41)
• Computing limit as x approaches some number or infinity (16 messages, latest: Oct 25 2020 at 22:26)
• Degree of the remainder of polynomial division (3 messages, latest: Oct 25 2020 at 03:28)
• Tactic for unions, intersections (36 messages, latest: Oct 24 2020 at 21:20)
• extension of scalars (8 messages, latest: Oct 24 2020 at 17:26)
• finset.fold of option.lift_or_get (8 messages, latest: Oct 23 2020 at 20:10)
• Product of a reversed list is inverse of product of inverses (72 messages, latest: Oct 23 2020 at 15:06)
• Formal partial derivative (3 messages, latest: Oct 23 2020 at 09:25)
• Single variable complex analysis (127 messages, latest: Oct 22 2020 at 20:57)
• {0, …, (i : fin n)} (42 messages, latest: Oct 22 2020 at 13:58)
• [monomial (n a) = aX^n](topic/monomial.20(n.20a).20.3D.20aX.5En.html) (22 messages, latest: Oct 22 2020 at 08:33)
• an abel-like tactic for nat? (7 messages, latest: Oct 22 2020 at 00:19)
• Absolute value for cardinality (12 messages, latest: Oct 21 2020 at 23:04)
• non-dense orders (13 messages, latest: Oct 21 2020 at 12:15)
• dependent type in inductive variant? (56 messages, latest: Oct 18 2020 at 17:27)
• infinite sequence (10 messages, latest: Oct 18 2020 at 12:19)
• sheafification of presheaf of ab groups (28 messages, latest: Oct 18 2020 at 04:07)
• Locally convex spaces and convinient vector spaces (4 messages, latest: Oct 17 2020 at 11:17)
• big_operators and bijections (10 messages, latest: Oct 17 2020 at 04:27)
• Basic cardinality calculation (34 messages, latest: Oct 16 2020 at 20:14)
• A bundled version of pow.is_monoid_hom? (3 messages, latest: Oct 15 2020 at 14:42)
• finsupp.sum commutes with monoid_hom (18 messages, latest: Oct 15 2020 at 10:09)
• signed (fin 2^n) ? (5 messages, latest: Oct 15 2020 at 06:44)
• Canonical subsets of sum (22 messages, latest: Oct 13 2020 at 15:39)
• Möbius function (6 messages, latest: Oct 13 2020 at 07:56)
• continuous_linear_equiv (15 messages, latest: Oct 12 2020 at 15:55)
• pattern matching prop? (78 messages, latest: Oct 12 2020 at 06:29)
• int.bit1_ne_zero (1 message, latest: Oct 11 2020 at 20:13)
• has_sum of partial sums (5 messages, latest: Oct 11 2020 at 08:46)
• Destruct multiple disjunctions (9 messages, latest: Oct 11 2020 at 07:15)
• colimit of Hom (12 messages, latest: Oct 10 2020 at 18:53)
• finset α from finset (α⊕ β) (12 messages, latest: Oct 10 2020 at 09:14)
• is_basis + is_scalar_tower (2 messages, latest: Oct 10 2020 at 06:56)
• Submodules of polynomial rings of bounded degree (2 messages, latest: Oct 09 2020 at 21:21)
• summable_abs_iff (2 messages, latest: Oct 09 2020 at 04:41)
• More point set topology questions (38 messages, latest: Oct 08 2020 at 22:49)
• is_open_iff_ultrafilter (7 messages, latest: Oct 08 2020 at 08:26)
• swapping exists and or (33 messages, latest: Oct 08 2020 at 00:38)
• subtype.coind for linear_map and other homs? (3 messages, latest: Oct 07 2020 at 14:35)
• defining a polynomial (7 messages, latest: Oct 06 2020 at 23:03)
• Parser combinators (5 messages, latest: Oct 06 2020 at 22:28)
• Pi (41 messages, latest: Oct 06 2020 at 22:00)
• Closure of set of sets under finite intersections (4 messages, latest: Oct 06 2020 at 21:15)
• Simple set theory nonsense (13 messages, latest: Oct 06 2020 at 15:28)
• subset of finset is finite (10 messages, latest: Oct 06 2020 at 13:15)
• equivalent formulation of "is not divisible" (2 messages, latest: Oct 06 2020 at 03:04)
• smallest element of a set? (28 messages, latest: Oct 05 2020 at 22:29)
• A lemma about ultrafilters (3 messages, latest: Oct 05 2020 at 14:24)
• Semigroup morphisms (22 messages, latest: Oct 05 2020 at 09:36)
• head of a list? (6 messages, latest: Oct 05 2020 at 08:00)
• mv_power_series (12 messages, latest: Oct 04 2020 at 21:02)
• tactic to eliminate double negation (24 messages, latest: Oct 04 2020 at 18:17)
• A polynomial splits if it has enough roots (11 messages, latest: Oct 04 2020 at 10:41)
• typeof (3 messages, latest: Oct 04 2020 at 00:56)
• bidirectional maps? (93 messages, latest: Oct 02 2020 at 06:39)
• Subgroups of the integers (9 messages, latest: Oct 02 2020 at 04:18)
• Insert lemmas (3 messages, latest: Oct 01 2020 at 17:42)
• bit mod two (6 messages, latest: Oct 01 2020 at 08:35)
• algebra.adjoin is subring.closure (6 messages, latest: Sep 30 2020 at 16:25)
• Induction over a generating set (9 messages, latest: Sep 30 2020 at 13:57)
• mul_left_cancel' for modules (5 messages, latest: Sep 30 2020 at 03:10)
• cardinality of set of fintype? (9 messages, latest: Sep 29 2020 at 06:02)
• semiring+algebra => ring (22 messages, latest: Sep 28 2020 at 09:55)
• p divides x-x^p (9 messages, latest: Sep 26 2020 at 22:45)
• Symmetric Functions (3 messages, latest: Sep 25 2020 at 22:30)
• Monoid instance on End(X) (3 messages, latest: Sep 25 2020 at 16:26)
• quotient by monoid action (59 messages, latest: Sep 24 2020 at 17:08)
• has_limits of has_limits and creates_limits (7 messages, latest: Sep 24 2020 at 14:26)
• involutive f ↔ f ∘ f = id (32 messages, latest: Sep 24 2020 at 14:10)
• Pushforward(?) topology (3 messages, latest: Sep 24 2020 at 13:48)
• dvd_of_pow_dvd_pow (2 messages, latest: Sep 24 2020 at 07:34)
• interweaved list (8 messages, latest: Sep 23 2020 at 17:29)
• S1 and other topological spaces (37 messages, latest: Sep 22 2020 at 23:58)
• Fibered products (7 messages, latest: Sep 22 2020 at 21:34)
• auto-coercions (24 messages, latest: Sep 21 2020 at 21:46)
• Gcd type tags (14 messages, latest: Sep 21 2020 at 21:18)
• Functor preserving binary products (13 messages, latest: Sep 21 2020 at 15:08)
• monad question (14 messages, latest: Sep 20 2020 at 05:34)
• Copying projections through a definition (2 messages, latest: Sep 17 2020 at 18:31)
• rw part of an inequality (14 messages, latest: Sep 16 2020 at 15:00)
• cast_card_eq_zero (1 message, latest: Sep 16 2020 at 09:21)
• nat.pow_pos (5 messages, latest: Sep 15 2020 at 19:23)
• implication on bool (5 messages, latest: Sep 15 2020 at 14:49)
• suppress an hyptohesis (12 messages, latest: Sep 15 2020 at 08:44)
• Setoid associated to filter (15 messages, latest: Sep 14 2020 at 20:34)
• Multiset to set (42 messages, latest: Sep 14 2020 at 09:49)
• how do I activate sum.lex? (3 messages, latest: Sep 14 2020 at 08:57)
• sq_sub_sq for nat (8 messages, latest: Sep 13 2020 at 21:29)
• Tail of bounded series tends to zero (2 messages, latest: Sep 12 2020 at 20:15)
• Subalgebras over different base fields (4 messages, latest: Sep 10 2020 at 22:49)
• continuous map to \top (3 messages, latest: Sep 10 2020 at 17:27)
• nat.rec_succ (5 messages, latest: Sep 10 2020 at 14:21)
• base change of module (20 messages, latest: Sep 09 2020 at 20:57)
• R is the unique complete archimedean ordered field (7 messages, latest: Sep 08 2020 at 16:49)
• Coprime numbers whose product is a square are both square (8 messages, latest: Sep 08 2020 at 16:13)
• Mapping ideals to localizations (3 messages, latest: Sep 07 2020 at 15:42)
• associates R -> ideal R (1 message, latest: Sep 06 2020 at 16:59)
• single-valued relation (2 messages, latest: Sep 06 2020 at 15:57)
• at_top for an interval (8 messages, latest: Sep 04 2020 at 23:15)
• comp_apply for concrete categories (3 messages, latest: Sep 04 2020 at 13:06)
• Fermat's right triangle theorem (9 messages, latest: Sep 04 2020 at 08:39)
• linear dependence of more than dimension (46 messages, latest: Sep 03 2020 at 10:19)
• fincard X^Y (2 messages, latest: Sep 03 2020 at 04:51)
• p-adic integers as inverse limit (7 messages, latest: Sep 02 2020 at 14:30)
• I-adic valuation on R (18 messages, latest: Sep 02 2020 at 13:17)
• if f o g is linearly independent then so is g (2 messages, latest: Sep 01 2020 at 15:50)
• Galois fields or Elliptic curves? (6 messages, latest: Sep 01 2020 at 12:14)
• vector.prod (2 messages, latest: Sep 01 2020 at 11:57)
• localization away from f (5 messages, latest: Sep 01 2020 at 03:32)
• fintype.induction_on (32 messages, latest: Aug 29 2020 at 19:43)
• has_mem for subgroups of units (10 messages, latest: Aug 27 2020 at 19:57)
• pull back an R module along S ->+* R (35 messages, latest: Aug 26 2020 at 12:33)
• line break in tactic.pp (5 messages, latest: Aug 26 2020 at 12:25)
• integral and linear maps (1 message, latest: Aug 25 2020 at 22:10)
• apply linear_map (1 message, latest: Aug 25 2020 at 21:14)
• infinite sums of functions (10 messages, latest: Aug 25 2020 at 20:48)
• finsupp gsmul_eq_smul (9 messages, latest: Aug 25 2020 at 17:55)
• Transfer instance through equivalences (11 messages, latest: Aug 25 2020 at 11:58)
• Category instance on Sigma type (3 messages, latest: Aug 24 2020 at 23:06)
• Status of Spectral Theorem? (109 messages, latest: Aug 24 2020 at 21:57)
• rewrite at a specific variable? (10 messages, latest: Aug 24 2020 at 20:00)
• quotient by product relation (16 messages, latest: Aug 24 2020 at 19:58)
• Pythagoras' Theorem (3 messages, latest: Aug 23 2020 at 17:02)
• "Archimedean minimal" (3 messages, latest: Aug 21 2020 at 22:24)
• multiset.nodup s ↔ ∀ a t, s ≠ a :: a :: t (3 messages, latest: Aug 20 2020 at 07:07)
• Hyperbolic Trig Functions (18 messages, latest: Aug 18 2020 at 11:02)
• Set coercion (8 messages, latest: Aug 17 2020 at 20:18)
• Order topology (17 messages, latest: Aug 17 2020 at 18:57)
• category of POSet (12 messages, latest: Aug 17 2020 at 17:27)
• Gram-Schmidt orthogonalization (28 messages, latest: Aug 16 2020 at 19:14)
• Krull's Theorem (5 messages, latest: Aug 16 2020 at 17:17)
• category of sets (17 messages, latest: Aug 15 2020 at 13:19)
• maximal ideals in integral extensions (5 messages, latest: Aug 15 2020 at 09:31)
• fintype.equiv_congr (19 messages, latest: Aug 15 2020 at 05:05)
• Isomorphisms of categories (16 messages, latest: Aug 14 2020 at 22:44)
• Ordered groups have no top element (8 messages, latest: Aug 14 2020 at 20:15)
• fast div and mod (5 messages, latest: Aug 12 2020 at 15:51)
• Iterated product is multilinear (2 messages, latest: Aug 12 2020 at 15:39)
• initial / final functors (5 messages, latest: Aug 12 2020 at 13:33)
• Left and right inverse of function (2 messages, latest: Aug 12 2020 at 00:50)
• Morphisms of monads (72 messages, latest: Aug 11 2020 at 22:59)
• Predicates on predicates involving instances (4 messages, latest: Aug 10 2020 at 07:43)
• polynomial comp and map (7 messages, latest: Aug 10 2020 at 06:45)
• linear_order compatible with a given partial_order (2 messages, latest: Aug 09 2020 at 06:53)
• invertible modules are f.g. (2 messages, latest: Aug 09 2020 at 04:58)
• Composition ring (2 messages, latest: Aug 08 2020 at 23:36)
• Lattice induced by order isomorphism (2 messages, latest: Aug 08 2020 at 21:34)
• Lift of binary function (27 messages, latest: Aug 08 2020 at 20:08)
• sum of products (5 messages, latest: Aug 08 2020 at 01:58)
• simplicial sets (10 messages, latest: Aug 07 2020 at 19:21)
• findim = 1 (7 messages, latest: Aug 07 2020 at 17:19)
• Effect of changing the base field on span (17 messages, latest: Aug 07 2020 at 10:15)
• Goodstein's theorem (2 messages, latest: Aug 06 2020 at 23:45)
• intervals are infinite (12 messages, latest: Aug 06 2020 at 19:39)
• reals are unique (4 messages, latest: Aug 06 2020 at 16:55)
• group_with_zero (with_zero G) (6 messages, latest: Aug 06 2020 at 14:15)
• use mathlib branch in project (5 messages, latest: Aug 05 2020 at 00:55)
• Ideals over algebras (139 messages, latest: Aug 04 2020 at 18:06)
• Distrib lattice constructors (4 messages, latest: Aug 03 2020 at 05:46)
• Big op products with rearranged indices (3 messages, latest: Aug 02 2020 at 13:07)
• Finite dimensional vector space over a finite field (28 messages, latest: Jul 30 2020 at 18:31)
• manipulating multiset elements in proof (10 messages, latest: Jul 29 2020 at 18:20)
• Sheaves of category-objects (68 messages, latest: Jul 29 2020 at 16:57)
• reverse ∘ take = drop ∘ reverse (10 messages, latest: Jul 28 2020 at 13:46)
• union of list of finsets (18 messages, latest: Jul 28 2020 at 08:53)
• (list.cons a l) ≠ l (35 messages, latest: Jul 27 2020 at 19:11)
• a lemma about –inducing– open_embedding? (1 message, latest: Jul 27 2020 at 13:59)
• a lemma about inducing? (16 messages, latest: Jul 27 2020 at 13:51)
• mul_linear_map (7 messages, latest: Jul 27 2020 at 09:31)
• Tangent Space of Sphere (1 message, latest: Jul 26 2020 at 17:36)
• Automating over structures (6 messages, latest: Jul 25 2020 at 04:29)
• monoid object (18 messages, latest: Jul 25 2020 at 02:56)
• std_basis (3 messages, latest: Jul 24 2020 at 20:45)
• Right inverse of injective (3 messages, latest: Jul 24 2020 at 17:34)
• mulabel (3 messages, latest: Jul 23 2020 at 09:11)
• dfinsupp of product is dfinsupp of dfinsupp (13 messages, latest: Jul 22 2020 at 12:14)
• locally ringed spaces (1 message, latest: Jul 22 2020 at 09:27)
• Local vs global minimum (17 messages, latest: Jul 20 2020 at 02:58)
• decidable search on a list (5 messages, latest: Jul 19 2020 at 15:54)
• int.coe_to_nat_eq (4 messages, latest: Jul 19 2020 at 11:29)
• symmetric.iff (3 messages, latest: Jul 19 2020 at 05:07)
• All but last element of a list (8 messages, latest: Jul 18 2020 at 18:54)
• Linear combinations stay in a submodule (10 messages, latest: Jul 18 2020 at 17:32)
• Z/nZ = zmod? (1 message, latest: Jul 18 2020 at 10:59)
• fderiv is 0 if derivative is 0 (8 messages, latest: Jul 15 2020 at 21:12)
• Automatic intro/cases/specialize/use dance (31 messages, latest: Jul 15 2020 at 19:25)
• recovering from an exists (11 messages, latest: Jul 13 2020 at 01:06)
• finite fields (41 messages, latest: Jul 11 2020 at 06:29)
• How best to express my applied maths problem in mathlib? (5 messages, latest: Jul 10 2020 at 13:47)
• Disjoint union of fin's (6 messages, latest: Jul 10 2020 at 00:42)
• quotient by bottom setoid (5 messages, latest: Jul 09 2020 at 19:12)
• is_unit_group (4 messages, latest: Jul 09 2020 at 10:27)
• Apply function N times (23 messages, latest: Jul 07 2020 at 20:51)
• list (option α) → list α (27 messages, latest: Jul 07 2020 at 19:47)
• list.split_sum (7 messages, latest: Jul 07 2020 at 19:47)
• list operation (9 messages, latest: Jul 05 2020 at 18:08)
• sum_sum_elim for fintypes (16 messages, latest: Jul 05 2020 at 17:07)
• Lean, show me the first 5 elements in the set of natural num (10 messages, latest: Jul 04 2020 at 20:11)
• add_monoid_hom.cod_restrict (1 message, latest: Jul 04 2020 at 19:27)
• bundled one-sided invertible functions (7 messages, latest: Jul 02 2020 at 14:22)
• Doing differential geometry (10 messages, latest: Jul 01 2020 at 03:11)
• A boolean algebra is an ordered comm monoid (15 messages, latest: Jun 30 2020 at 06:49)
• Finite geometric series (43 messages, latest: Jun 29 2020 at 03:01)
• isomorphisms define category (3 messages, latest: Jun 29 2020 at 00:27)
• nonzero (fin n.succ.succ) (8 messages, latest: Jun 28 2020 at 23:01)
• Statement of Cauchy's integral formula (4 messages, latest: Jun 28 2020 at 04:22)
• Rigs and rings (2 messages, latest: Jun 28 2020 at 04:14)
• Equal within s imply same limit within s (65 messages, latest: Jun 27 2020 at 20:14)
• telescoping sums (35 messages, latest: Jun 26 2020 at 13:37)
• Redefining Operators (21 messages, latest: Jun 26 2020 at 03:24)
• Injective on a set up to a relation (10 messages, latest: Jun 25 2020 at 19:45)
• Is there code for Galois theory? (60 messages, latest: Jun 24 2020 at 08:47)
• Decompose a natural into perfect square (4 messages, latest: Jun 23 2020 at 23:36)
• fdvs lemmas (23 messages, latest: Jun 23 2020 at 00:38)
• finsupp tensor finsupp (8 messages, latest: Jun 22 2020 at 23:59)
• finsupp is direct sum (6 messages, latest: Jun 22 2020 at 23:50)
• Results on gcd (8 messages, latest: Jun 20 2020 at 22:32)
• prod_ite_eq (11 messages, latest: Jun 18 2020 at 15:14)
• Cartesian Closed Categories (6 messages, latest: Jun 16 2020 at 03:50)
• order on bool (11 messages, latest: Jun 15 2020 at 01:01)
• pretty printing an expr (4 messages, latest: Jun 14 2020 at 16:05)
• add_comm_group tactic? (19 messages, latest: Jun 14 2020 at 04:05)
• Usual topology on R (6 messages, latest: Jun 12 2020 at 13:42)
• if the dual of a well order is also a well order then finite (13 messages, latest: Jun 11 2020 at 08:06)
• a well-ordered subset of \R is countable (4 messages, latest: Jun 11 2020 at 07:56)
• Linear combination description of span (3 messages, latest: Jun 10 2020 at 21:58)
• A finite division ring is a field (11 messages, latest: Jun 09 2020 at 07:01)
• 0 ≤ x * x + y * y again (14 messages, latest: Jun 08 2020 at 15:11)
• Identify span of vector with field (12 messages, latest: Jun 08 2020 at 05:08)
• Preimage of finite sets (32 messages, latest: Jun 06 2020 at 20:19)
• f(x)=q(x)(x-r) + f(r) (16 messages, latest: Jun 02 2020 at 19:45)
• has_mem for subtype (23 messages, latest: Jun 02 2020 at 14:00)
• trunc (14 messages, latest: Jun 02 2020 at 06:22)
• N epsilon convergence of sqnce in metric space (37 messages, latest: May 29 2020 at 10:09)
• Sup and Inf in R have sequences converging to them (3 messages, latest: May 29 2020 at 05:12)
• Making homs in CommRing (12 messages, latest: May 26 2020 at 10:40)
• matrices over a ring are a ring (64 messages, latest: May 26 2020 at 04:19)
• finset.sum_apply' (16 messages, latest: May 25 2020 at 16:04)
• intro h, cases h with p q where h : p ∨ q (10 messages, latest: May 24 2020 at 21:31)
• card_le_of (9 messages, latest: May 24 2020 at 20:09)
• nat subtraction hurts (20 messages, latest: May 24 2020 at 19:23)
• dim_le_of (5 messages, latest: May 24 2020 at 15:48)
• polynomial.eq_of_monic_of_associated (4 messages, latest: May 24 2020 at 08:16)
• quot.lift₂ (12 messages, latest: May 23 2020 at 21:29)
• zmod (21 messages, latest: May 23 2020 at 14:39)
• mul_dvd_of_coprime (2 messages, latest: May 23 2020 at 14:24)
• finset.erase_singleton_self (10 messages, latest: May 23 2020 at 13:24)
• inequalities for fintype.card (10 messages, latest: May 22 2020 at 14:57)
• int.sub_mod (11 messages, latest: May 22 2020 at 11:03)
• x^2+y^2>=0 (14 messages, latest: May 21 2020 at 16:14)
• lifting α ↪ α to α ≃ α in the presence of fintype α? (5 messages, latest: May 21 2020 at 01:17)
• linear maps between algebra modules form a module over … (5 messages, latest: May 20 2020 at 11:49)
• eq_iff_modeq_int (40 messages, latest: May 18 2020 at 14:04)
• gcd ind? (10 messages, latest: May 17 2020 at 08:58)
• function.injective_of_left_inverse (2 messages, latest: May 16 2020 at 17:34)
• total order (20 messages, latest: May 16 2020 at 14:39)
• Borel determinacy (46 messages, latest: May 16 2020 at 14:01)
• a mutable tactic (22 messages, latest: May 16 2020 at 12:09)
• Ideals of an algebra are submodules (16 messages, latest: May 14 2020 at 14:33)
• List lemmas (14 messages, latest: May 12 2020 at 10:40)
• sequence tending to a limit (10 messages, latest: May 10 2020 at 18:38)
• subtype.property' (2 messages, latest: May 06 2020 at 13:18)
• basis of free module X -> R with [fintype X]? (4 messages, latest: May 02 2020 at 12:08)
• projectors (13 messages, latest: Apr 30 2020 at 23:27)
• real powers of positive reals? (17 messages, latest: Apr 30 2020 at 15:01)
• bnot (a && b) = (bnot a) || (bnot b) (27 messages, latest: Apr 25 2020 at 19:48)
• exporting a program's AST (10 messages, latest: Apr 25 2020 at 02:25)
• enumerating a fintype (6 messages, latest: Apr 23 2020 at 05:21)
• last n elements of a list (10 messages, latest: Apr 21 2020 at 09:35)
• continuous functions commute with limits? (15 messages, latest: Apr 19 2020 at 19:25)
• list.is_palindrome (6 messages, latest: Apr 19 2020 at 00:11)
• Density of Q in R (8 messages, latest: Apr 17 2020 at 13:11)
• nat.eq_div_of_mul_eq (44 messages, latest: Apr 16 2020 at 14:24)
• undergraduate calculus (81 messages, latest: Apr 15 2020 at 12:18)
• algebra R (monoid_algebra R G) (21 messages, latest: Apr 15 2020 at 01:40)
• definite and indefinite integrals on the reals (7 messages, latest: Apr 14 2020 at 19:18)
• Bolzano-Weirstrass (89 messages, latest: Apr 12 2020 at 11:33)
• fintype (s.to_set) (6 messages, latest: Apr 12 2020 at 10:54)
• add_left_cancel_monoid (16 messages, latest: Apr 10 2020 at 07:43)
• high scores (24 messages, latest: Apr 05 2020 at 12:04)
• Multiplicative group of integers modulo n (12 messages, latest: Mar 15 2020 at 02:54)
• Sorted set (2 messages, latest: Mar 01 2020 at 10:06)
• If there is an inverse, it's unique? (2 messages, latest: Feb 26 2020 at 11:30)
• distance preserving maps (12 messages, latest: Feb 24 2020 at 19:48)
• General linear groups (3 messages, latest: Feb 21 2020 at 23:20)
• smul_comm (1 message, latest: Feb 10 2020 at 18:59)
• mem_span if finite linear combination (4 messages, latest: Feb 10 2020 at 09:56)
• Getting instance from parent instance (2 messages, latest: Feb 09 2020 at 15:59)
• representation theory of finite groups (4 messages, latest: Jan 17 2020 at 05:52)
• the trace of a square matrix (1 message, latest: Jan 15 2020 at 22:44)
• valuation rings (3 messages, latest: Dec 30 2019 at 09:15)
• Completion of a ring (2 messages, latest: Dec 23 2019 at 15:38)
• Super vector space (1 message, latest: Dec 22 2019 at 14:10)

---

Last updated: Dec 20 2023 at 11:08 UTC