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 amonoid_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 anint
(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
andp.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 oversum
(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
iffin 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
toa * 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 α
fromfinset (α⊕ β)
(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
forlinear_map
and otherhom
s? (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 givenpartial_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
whereh : 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 offintype α
? (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