Zulip Chat Archive

Stream: Is there code for X?

Topics:

Minkowski Lattice Theorem (6 messages, latest: Apr 16 2021 at 17:23)
convex hulls and compact convex sets (27 messages, latest: Apr 16 2021 at 05:28)
continuous_on.dif (13 messages, latest: Apr 15 2021 at 21:18)
Birthday Problem (19 messages, latest: Apr 15 2021 at 17:44)
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)
Open set of reals contains ball/interval (21 messages, latest: Apr 15 2021 at 14:26)
submonoid.mem_supr (3 messages, latest: Apr 15 2021 at 13:44)
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)
rational functions (9 messages, latest: Apr 13 2021 at 05:23)
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)
mul_neg, neg_mul (3 messages, latest: Apr 08 2021 at 11:45)
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)
Dirichlet's theorem on arithmetic progressions? (12 messages, latest: Apr 02 2021 at 08:25)
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)
(no topic) (13 messages, latest: Mar 31 2021 at 14:17)
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)
Do we have CW complexes? (48 messages, latest: Mar 27 2021 at 17:51)
nat.log_mono (7 messages, latest: Mar 26 2021 at 20:49)
"backwards" induction on fin (2 messages, latest: Mar 26 2021 at 15:44)
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)
R^m is finite dimensional over R (28 messages, latest: Mar 25 2021 at 04:57)
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)
Continuous algebra homomorphisms (28 messages, latest: Mar 18 2021 at 21:02)
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)
Lattice Homomorphisms? (19 messages, latest: Mar 14 2021 at 16:25)
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)
Continuous bijective from compact to T1 implies homeomorphis (4 messages, latest: Mar 10 2021 at 13:20)
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)
unique from empty (40 messages, latest: Mar 02 2021 at 07:14)
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)
symmetric difference / disjunctive union of sets (45 messages, latest: Feb 28 2021 at 08:22)
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)
inf_Sup_right (27 messages, latest: Feb 25 2021 at 13:12)
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)
[specialize h , swap](topic/specialize.20h.20.2C.20swap.html) (5 messages, latest: Feb 09 2021 at 22:29)
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)
extension of scalars for a module, complexification (7 messages, latest: Jan 14 2021 at 13:03)
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)
separable/purely inseparable extension and separable closure (8 messages, latest: Dec 29 2020 at 16:35)
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)
profinite sets (35 messages, latest: Dec 02 2020 at 15:21)
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)
prefunctor? (107 messages, latest: Oct 29 2020 at 06:07)
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)
Well-ordering of the integers (4 messages, latest: Sep 29 2020 at 18:01)
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)
Moore-Smith sequences (3 messages, latest: Sep 23 2020 at 14:59)
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)
Partial derivatives (9 messages, latest: Aug 23 2020 at 19:18)
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)
Graph Theory (154 messages, latest: Aug 06 2020 at 04:08)
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)
Simple ring lemma (39 messages, latest: Jul 08 2020 at 19:31)
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)
transcendence of pi (10 messages, latest: Jul 01 2020 at 17:05)
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)
kTop is CCC (9 messages, latest: Jun 16 2020 at 11:37)
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)
Calculations with presheaves (36 messages, latest: Jun 01 2020 at 15:31)
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)
random number generator (13 messages, latest: May 15 2020 at 22:17)
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)
stream events (1 message, latest: Dec 22 2019 at 14:08)

Last updated: Apr 16 2021 at 19:18 UTC