Zulip Chat Archive

Stream: Is there code for X?

Topics:

Factorization algebras (13 messages, latest: Jun 19 2021 at 18:36)
R[X] is an R-algebra (6 messages, latest: Jun 19 2021 at 13:20)
e as limit of (1+1/n)^n (9 messages, latest: Jun 18 2021 at 19:25)
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 induced by left composition (8 messages, latest: Jun 18 2021 at 05:53)
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)
nat.factorial lemmas (39 messages, latest: May 30 2021 at 13:49)
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)
real.log in other base (5 messages, latest: May 05 2021 at 08:35)
set to finset equiv (15 messages, latest: May 05 2021 at 06:28)
monoid instance on self maps (22 messages, latest: May 04 2021 at 21:54)
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)
Endomorphism of ring over itself (2 messages, latest: May 02 2021 at 07:55)
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)
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)
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)
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)
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)
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)
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)
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: Jun 20 2021 at 02:05 UTC