Zulip Chat Archive
Stream: Is there code for X?
Topics:
- quotient.lift_on_family (22 messages, latest: Jan 31 2023 at 18:09)
- Ring of integers is a free β€-module (17 messages, latest: Jan 31 2023 at 14:38)
- Prime number theorem (42 messages, latest: Jan 31 2023 at 08:51)
- β pigeonhole (16 messages, latest: Jan 29 2023 at 22:33)
- Partition numbers (9 messages, latest: Jan 29 2023 at 01:32)
- Proving Pell's equation is solvable (18 messages, latest: Jan 27 2023 at 17:41)
- int.cast for fin (5 messages, latest: Jan 27 2023 at 15:08)
- Topology on infinite sequence spaces (10 messages, latest: Jan 27 2023 at 14:21)
- ordinals and induction (55 messages, latest: Jan 27 2023 at 14:14)
- Convex implies monotone secants (15 messages, latest: Jan 25 2023 at 21:42)
- coe summable (6 messages, latest: Jan 25 2023 at 19:52)
- Euclidean Geometry (112 messages, latest: Jan 24 2023 at 00:45)
- β Icc_ge_subsingleton (13 messages, latest: Jan 23 2023 at 08:34)
- X^d - 1 | X^(nd) - 1 (17 messages, latest: Jan 22 2023 at 03:20)
- sensible constructor for
add_comm_group
(17 messages, latest: Jan 20 2023 at 21:40) - premeasures (1 message, latest: Jan 20 2023 at 16:04)
- zero module (9 messages, latest: Jan 19 2023 at 22:48)
- coefft of X^j in prod_i (X + a_i) (8 messages, latest: Jan 19 2023 at 22:44)
- existence of equiv mapping nodup same length lists (17 messages, latest: Jan 19 2023 at 08:30)
- Adjoin_root
f
is a domain for primef
(5 messages, latest: Jan 18 2023 at 23:11) - make an argument implicit (5 messages, latest: Jan 18 2023 at 22:37)
- Maximum Term Method Help (7 messages, latest: Jan 16 2023 at 21:58)
- Biratio (9 messages, latest: Jan 16 2023 at 20:18)
- Do mathlib have at_top_bot filter (3 messages, latest: Jan 15 2023 at 11:43)
- strongly_measurable.is_lub (8 messages, latest: Jan 14 2023 at 17:02)
- Affine space over vector span (2 messages, latest: Jan 14 2023 at 13:44)
- π½β (17 messages, latest: Jan 12 2023 at 23:08)
- Abel's summation and/or Stieltjes integration (5 messages, latest: Jan 12 2023 at 11:52)
- Equality of ideals from local equality (4 messages, latest: Jan 12 2023 at 11:13)
- Geometry Of Numbers (16 messages, latest: Jan 12 2023 at 05:09)
- β real affine maps (10 messages, latest: Jan 11 2023 at 14:50)
- real affine maps (2 messages, latest: Jan 11 2023 at 14:00)
- Ramsey Theory/Graphs (5 messages, latest: Jan 10 2023 at 18:22)
- Descartes Rule of Signs (31 messages, latest: Jan 09 2023 at 16:34)
- Notation precedence (1 message, latest: Jan 09 2023 at 16:25)
- Alexander's theorem (8 messages, latest: Jan 09 2023 at 05:26)
- Example Code of Matrix Rank (16 messages, latest: Jan 06 2023 at 11:28)
- Enlarge the codomain of a function (5 messages, latest: Jan 05 2023 at 23:13)
- Binomial theorem (28 messages, latest: Jan 05 2023 at 22:20)
- Lattices (the other kind) (4 messages, latest: Jan 05 2023 at 08:49)
- Complexity theory (335 messages, latest: Jan 05 2023 at 04:58)
- Dirichlet inverses (4 messages, latest: Jan 05 2023 at 00:45)
- β Two ways to sum finsets (14 messages, latest: Jan 04 2023 at 22:25)
- Ostrowski's theorem (21 messages, latest: Jan 04 2023 at 21:41)
- β Set Systems? (29 messages, latest: Jan 04 2023 at 14:11)
- Restricted well-foundedness of docs#prod.lex (4 messages, latest: Jan 04 2023 at 08:33)
- abv a - abv b β€ abv (a + b) (10 messages, latest: Jan 04 2023 at 00:21)
- β
ennreal.mul_div_mul_left
(15 messages, latest: Jan 03 2023 at 16:07) ennreal.mul_div_mul_left
(3 messages, latest: Jan 03 2023 at 15:00)- Subgroups of zmod (11 messages, latest: Jan 03 2023 at 09:40)
- Reassociating docs#mul_opposite.op (8 messages, latest: Jan 02 2023 at 11:41)
- forget some declaration (7 messages, latest: Jan 02 2023 at 09:36)
- β case splitting in linear order? (13 messages, latest: Jan 01 2023 at 17:20)
- case splitting in linear order? (3 messages, latest: Jan 01 2023 at 16:39)
- [Hyperoperation and 2+2=22=2^2=β¦](topic/Hyperoperation.20and.202.2B2.3D22.3D2.5E2.3D.2E.2E.2E.html) (4 messages, latest: Jan 01 2023 at 03:28)
- Universal Algebra (13 messages, latest: Dec 30 2022 at 15:43)
- Power basis of
adjoin R x
(24 messages, latest: Dec 29 2022 at 18:00) - β finset on linear order to list? (3 messages, latest: Dec 29 2022 at 13:33)
- finset on linear order to list? (1 message, latest: Dec 29 2022 at 12:39)
- le.to_submodule (3 messages, latest: Dec 28 2022 at 19:51)
- β Tactic similar to
apply
but generates equalities (2 messages, latest: Dec 27 2022 at 18:16) - Tactic similar to
apply
but generates equalities (4 messages, latest: Dec 27 2022 at 17:53) - β does lean have assert? (2 messages, latest: Dec 25 2022 at 02:00)
- Continuity from filters (25 messages, latest: Dec 24 2022 at 15:30)
- does lean have assert? (4 messages, latest: Dec 24 2022 at 14:28)
- divisibilty of powers (38 messages, latest: Dec 24 2022 at 12:49)
- Set is finite if image and fibers are finite? (7 messages, latest: Dec 24 2022 at 11:34)
- β
list.take_while_coe
? (1 message, latest: Dec 21 2022 at 10:57) - Set Systems? (18 messages, latest: Dec 21 2022 at 09:49)
list.take_while_coe
? (44 messages, latest: Dec 21 2022 at 09:29)- β
a β€ a + b
in ennreals (29 messages, latest: Dec 21 2022 at 07:30) - Primes > 2 are odd (16 messages, latest: Dec 20 2022 at 22:51)
- Conjugate elements in same Galois orbit (18 messages, latest: Dec 19 2022 at 18:11)
- Taking element from non-empty set (9 messages, latest: Dec 19 2022 at 14:38)
- logic.relation.symm_gen equivalent (5 messages, latest: Dec 17 2022 at 21:27)
- β is_open {a} from finite balls (3 messages, latest: Dec 17 2022 at 16:20)
- is_open {a} from finite balls (7 messages, latest: Dec 17 2022 at 15:54)
- Tactic to "name" a goal and use it afterwards (6 messages, latest: Dec 17 2022 at 14:44)
- access raw proof terms (6 messages, latest: Dec 17 2022 at 01:01)
- Permutation to make a function monotone (12 messages, latest: Dec 16 2022 at 17:48)
- β Cofinite maps? (25 messages, latest: Dec 16 2022 at 17:29)
- β setup option for simplifier
trace_lemmas
(8 messages, latest: Dec 15 2022 at 11:33) - The set of finite sets is well-founded? (23 messages, latest: Dec 14 2022 at 21:03)
- β finset to list (4 messages, latest: Dec 14 2022 at 05:36)
- Pulling
let
s to the outside of a statement (9 messages, latest: Dec 13 2022 at 13:16) - "backwards" induction on fin (3 messages, latest: Dec 13 2022 at 02:52)
- Isolated point (2 messages, latest: Dec 11 2022 at 14:23)
- If
a + b β€ 2 * c
then one of them isβ€ c
(33 messages, latest: Dec 11 2022 at 12:04) - β if list option has none then none (5 messages, latest: Dec 11 2022 at 07:01)
- Identifying endpoints of [0, 1] (17 messages, latest: Dec 10 2022 at 12:24)
- equiv from countable (6 messages, latest: Dec 10 2022 at 09:27)
- forgetting hypothesis definition (3 messages, latest: Dec 10 2022 at 07:29)
- Structures vs Type classes: Projections (8 messages, latest: Dec 08 2022 at 17:44)
- More general version of
list.map_const
? (8 messages, latest: Dec 08 2022 at 15:47) - Trichotomy of
int.sign
(15 messages, latest: Dec 06 2022 at 03:31) - β Showing 2 * int is not equal to 3 (6 messages, latest: Dec 05 2022 at 20:52)
- β Represent a ideal generated by an integer (3 messages, latest: Dec 05 2022 at 17:31)
- Represent a ideal generated by an integer (36 messages, latest: Dec 05 2022 at 12:29)
- Euclid's division lemma (6 messages, latest: Dec 01 2022 at 20:47)
- pi.monoid_hom (4 messages, latest: Nov 29 2022 at 20:46)
- β Declaring rings and ideals, and proving ideal is subset (10 messages, latest: Nov 29 2022 at 17:51)
- minimal polynomial of inverse (3 messages, latest: Nov 29 2022 at 16:02)
- Baire Category Stuff (1 message, latest: Nov 29 2022 at 12:59)
- Totient decidability (18 messages, latest: Nov 27 2022 at 18:45)
- β Is there a mul_left_inj for rings..? (3 messages, latest: Nov 26 2022 at 22:53)
- Is there a mul_left_inj for rings..? (9 messages, latest: Nov 26 2022 at 18:38)
- β
x β€ y \ z
fromdisjoint x z
andx β€ y
(2 messages, latest: Nov 26 2022 at 08:22) x β€ y \ z
fromdisjoint x z
andx β€ y
(3 messages, latest: Nov 26 2022 at 07:44)- multivariate chain rule for polynomials (4 messages, latest: Nov 23 2022 at 20:35)
- β Rewrite once (1 message, latest: Nov 23 2022 at 14:33)
- Rewrite once (15 messages, latest: Nov 23 2022 at 13:16)
- kTop is CCC (21 messages, latest: Nov 23 2022 at 00:32)
- Exporting all the proof terms (4 messages, latest: Nov 22 2022 at 15:25)
- β instance has_mul for structure (6 messages, latest: Nov 21 2022 at 20:47)
- β Is there a instance of "ring with (mul) inverse" (6 messages, latest: Nov 21 2022 at 16:49)
- fin.next (9 messages, latest: Nov 21 2022 at 07:46)
- Support functional (5 messages, latest: Nov 20 2022 at 09:48)
- coe_is_monoid_hom transitivity (9 messages, latest: Nov 19 2022 at 18:15)
- from rationals to reals (4 messages, latest: Nov 18 2022 at 22:49)
- Defining functions for structures (29 messages, latest: Nov 18 2022 at 17:44)
- "exactly one of the following is true" (11 messages, latest: Nov 18 2022 at 14:38)
- Intersection of localisations (26 messages, latest: Nov 18 2022 at 04:05)
- Inner product space on Ξ± Γ Ξ² (37 messages, latest: Nov 17 2022 at 10:39)
- Weights on polynomial rings, etc (4 messages, latest: Nov 17 2022 at 10:35)
- Reasoning about Algorithms (6 messages, latest: Nov 16 2022 at 23:00)
- Products of iterated derivatives (2 messages, latest: Nov 16 2022 at 14:37)
- pushforward/pullback of sheaves (14 messages, latest: Nov 16 2022 at 13:39)
- β lift a theorem on a type to a subtype? (5 messages, latest: Nov 15 2022 at 13:47)
- lift a theorem on a type to a subtype? (6 messages, latest: Nov 15 2022 at 13:08)
- β Mul eq implies a ne 0 (for div_ring) (4 messages, latest: Nov 15 2022 at 11:14)
- Mul eq implies a ne 0 (for div_ring) (3 messages, latest: Nov 15 2022 at 11:01)
- Obtain isomorphism from short exact sequence (40 messages, latest: Nov 14 2022 at 21:40)
- Is there a mul_lt_iff_lt_div (9 messages, latest: Nov 13 2022 at 17:28)
- β Is there a way to remove a hypothesis (4 messages, latest: Nov 12 2022 at 16:02)
- β Subtraction cancellation in a lt (4 messages, latest: Nov 12 2022 at 15:21)
- Subtraction cancellation in a lt (1 message, latest: Nov 12 2022 at 15:00)
- Product of integers is -1 [title changed] (6 messages, latest: Nov 12 2022 at 13:48)
- bottom type (β₯) (13 messages, latest: Nov 12 2022 at 03:22)
- eq_neg_iff_neg_eq? (23 messages, latest: Nov 11 2022 at 22:14)
no_confusion_heq
tactic? (21 messages, latest: Nov 11 2022 at 16:59)non_assoc_ring
is not amonoid_with_zero
? (32 messages, latest: Nov 11 2022 at 09:06)- Composition of algebras (5 messages, latest: Nov 11 2022 at 07:56)
- is_subgroup H G (10 messages, latest: Nov 10 2022 at 19:55)
- β
sum.map f g
is bijective if bothf
andg
are. (6 messages, latest: Nov 10 2022 at 17:39) sum.map f g
is bijective if bothf
andg
are. (3 messages, latest: Nov 10 2022 at 17:04)- Artinian/noetherian lattice (4 messages, latest: Nov 09 2022 at 13:55)
semiring
andcancel_comm_monoid_with_zero
(37 messages, latest: Nov 08 2022 at 18:40)- linear combination is in span (12 messages, latest: Nov 08 2022 at 00:31)
- list end-appending (4 messages, latest: Nov 07 2022 at 18:13)
- Instance management (8 messages, latest: Nov 07 2022 at 08:33)
- list.nodup iff length equal cardinality (8 messages, latest: Nov 06 2022 at 13:06)
- Small enough balls (11 messages, latest: Nov 05 2022 at 22:41)
- dirichlet character (4 messages, latest: Nov 03 2022 at 15:16)
- [specialize h , swap](topic/specialize.20h.20.2C.20swap.html) (10 messages, latest: Nov 03 2022 at 02:22)
- ae finite function of convergent integral (8 messages, latest: Nov 02 2022 at 19:03)
- re-casting to nat (11 messages, latest: Nov 01 2022 at 17:03)
- β list.join.take (1 message, latest: Nov 01 2022 at 16:36)
- folklore/"joke" theorem (8 messages, latest: Oct 31 2022 at 21:38)
- Contraposition Equivalence in Lean4 somewhere? (1 message, latest: Oct 28 2022 at 23:02)
- Operations on uniform limits (47 messages, latest: Oct 28 2022 at 17:10)
- Splitting a finite list as sublists (4 messages, latest: Oct 28 2022 at 13:54)
- Algebra trace equals sum of roots of charpoly (7 messages, latest: Oct 28 2022 at 12:04)
- 1 β -1 in β€Λ£? (22 messages, latest: Oct 27 2022 at 20:08)
- measurable_space β€Λ£ (3 messages, latest: Oct 26 2022 at 21:18)
- Preimage of defined subset of \R (8 messages, latest: Oct 26 2022 at 21:11)
- Finsupp generalisations (21 messages, latest: Oct 26 2022 at 19:03)
- β Left coset notation (26 messages, latest: Oct 26 2022 at 09:07)
- list.join.take (27 messages, latest: Oct 26 2022 at 09:00)
- Does Lean4 provide contraposition in somewhere? (1 message, latest: Oct 26 2022 at 02:12)
- β Is there a tactic to expand a forall (1 message, latest: Oct 25 2022 at 19:28)
- (p, q).snd (13 messages, latest: Oct 24 2022 at 20:43)
- Convention for the order on topologies (7 messages, latest: Oct 24 2022 at 19:10)
- Is there a tactic to expand a forall (3 messages, latest: Oct 24 2022 at 15:21)
- β "Big intersection" of sets (6 messages, latest: Oct 24 2022 at 15:13)
- Characterisation of connectedness using continuous maps (59 messages, latest: Oct 24 2022 at 14:47)
- β dense_inducing extension of uniform_continuous functions (2 messages, latest: Oct 24 2022 at 13:46)
- dense_inducing extension of uniform_continuous functions (12 messages, latest: Oct 24 2022 at 07:23)
- β eps-N rule for real (4 messages, latest: Oct 23 2022 at 20:50)
- Proper maps (in the sense of topology) (18 messages, latest: Oct 22 2022 at 15:31)
- Empty function (4 messages, latest: Oct 22 2022 at 15:23)
- β Unfolding the definition of a member of a smul (2 messages, latest: Oct 21 2022 at 20:01)
- Unfolding the definition of a member of a smul (7 messages, latest: Oct 21 2022 at 10:22)
- Open set of reals contains ball/interval (25 messages, latest: Oct 21 2022 at 07:54)
- Product of subgroups (5 messages, latest: Oct 21 2022 at 04:42)
- β Pull predicate from has_mem expr (6 messages, latest: Oct 20 2022 at 20:35)
- Pull predicate from has_mem expr (3 messages, latest: Oct 20 2022 at 20:16)
- β Finite types (1 message, latest: Oct 20 2022 at 19:30)
- β withType (4 messages, latest: Oct 20 2022 at 02:43)
- Complex roots of unity as a finset (18 messages, latest: Oct 20 2022 at 01:34)
- Permutation Models (3 messages, latest: Oct 19 2022 at 18:02)
- Ergodic maps / measures (5 messages, latest: Oct 18 2022 at 12:29)
- β Mapping injective function (3 messages, latest: Oct 18 2022 at 12:13)
- Locally uniform convergence (9 messages, latest: Oct 18 2022 at 00:00)
- sum over bigger finset (4 messages, latest: Oct 17 2022 at 23:21)
- Attribute Domains (4 messages, latest: Oct 17 2022 at 16:30)
- Check which imported definitions are used (4 messages, latest: Oct 17 2022 at 07:43)
- finsupp equals sum of
finsupp.filter
(2 messages, latest: Oct 15 2022 at 19:23) - Int version of caseswork of divisors (4 messages, latest: Oct 15 2022 at 17:08)
- Casts as actions (11 messages, latest: Oct 15 2022 at 16:00)
- kernel of a semiring action (17 messages, latest: Oct 15 2022 at 14:41)
- group with two elements (14 messages, latest: Oct 14 2022 at 01:49)
- Group (/monoid) rings (7 messages, latest: Oct 13 2022 at 11:43)
- How many elements of order two does S_4 have (7 messages, latest: Oct 12 2022 at 22:01)
- smooth vector field on manifold (1 message, latest: Oct 12 2022 at 21:46)
- free product of 2 groups (8 messages, latest: Oct 12 2022 at 21:15)
- mul_one_class, group⦠instances for dependend pi (5 messages, latest: Oct 12 2022 at 11:22)
- Equalities which are βthe wrong way roundβ involving bounβ¦ (9 messages, latest: Oct 11 2022 at 23:09)
tsum_ite_eq_extract
formonoid
(5 messages, latest: Oct 11 2022 at 19:13)to_prefunctor_ext
? (8 messages, latest: Oct 11 2022 at 16:49)- Computation of an explicit sum (11 messages, latest: Oct 11 2022 at 15:07)
- Accumulation point (61 messages, latest: Oct 10 2022 at 08:50)
- Module localization (10 messages, latest: Oct 10 2022 at 08:32)
- forgetting a hypothesis (2 messages, latest: Oct 08 2022 at 00:24)
- Extending well-founded relation to well-order (17 messages, latest: Oct 07 2022 at 23:05)
- coe from
finset.subtype
tofinset
(16 messages, latest: Oct 07 2022 at 04:15) - golf
nat.coprime
proof (20 messages, latest: Oct 06 2022 at 22:52) - Term representing match (10 messages, latest: Oct 06 2022 at 20:43)
- matrix.eq_zero_of_mul_eq_zero (4 messages, latest: Oct 06 2022 at 17:12)
- supremum of pointwise product of sets of real numbers (4 messages, latest: Oct 06 2022 at 14:09)
- Finite arithmetic progressions (28 messages, latest: Oct 06 2022 at 13:41)
- β
β (m : β€), - m * 2 β 1
(6 messages, latest: Oct 05 2022 at 15:55) - Vector of ones (3 messages, latest: Oct 05 2022 at 02:46)
- namespace in metaprogramming (5 messages, latest: Oct 05 2022 at 02:01)
- congruence of filters for tendsto (110 messages, latest: Oct 04 2022 at 18:37)
- continuity of derivative in a different argument (2 messages, latest: Oct 04 2022 at 05:54)
Ioo (a β b) a βo Ioo b (a β b)
(2 messages, latest: Oct 03 2022 at 08:46)- "sort" a function (79 messages, latest: Oct 03 2022 at 02:16)
- Hyperplane is closed or dense (3 messages, latest: Oct 02 2022 at 20:56)
- permutations preserving a function (14 messages, latest: Oct 02 2022 at 17:11)
- Lebesgue Density Theorem (7 messages, latest: Oct 02 2022 at 15:16)
- Uniform separation of compact and closed set (5 messages, latest: Oct 01 2022 at 20:04)
- Kaminski's Equation (67 messages, latest: Sep 30 2022 at 16:06)
- Finite state machines / transducers (5 messages, latest: Sep 30 2022 at 13:03)
- Simple ring lemma (42 messages, latest: Sep 29 2022 at 23:09)
- Help proving well_foundedness (13 messages, latest: Sep 28 2022 at 20:16)
- How to make a Blueprint (59 messages, latest: Sep 28 2022 at 16:34)
- Finite basis with small vectors (2 messages, latest: Sep 28 2022 at 08:35)
- name function without function body (5 messages, latest: Sep 28 2022 at 03:13)
- continuous on an open set (9 messages, latest: Sep 27 2022 at 22:07)
- Eliminate part of a product type from
tsum
(5 messages, latest: Sep 27 2022 at 16:23) - polynomial ext with degree bound (42 messages, latest: Sep 27 2022 at 14:38)
- galois insertion (co)atoms (2 messages, latest: Sep 26 2022 at 14:24)
- least element principle (8 messages, latest: Sep 25 2022 at 22:16)
- β Constant functions are analytic (2 messages, latest: Sep 25 2022 at 15:52)
- int.mod_by_nat (20 messages, latest: Sep 24 2022 at 00:16)
- Completion of a complete space (23 messages, latest: Sep 23 2022 at 19:40)
- Tensor products of inner product spaces (18 messages, latest: Sep 23 2022 at 14:48)
- exponential function to a natural power (4 messages, latest: Sep 23 2022 at 07:00)
- Subspace Topology (32 messages, latest: Sep 22 2022 at 23:53)
- composing functions (4 messages, latest: Sep 22 2022 at 22:14)
- Maximal independent set of a graph (3 messages, latest: Sep 22 2022 at 13:11)
- adding angles (80 messages, latest: Sep 22 2022 at 07:26)
- β List containing unique natural numbers (23 messages, latest: Sep 22 2022 at 07:22)
- fin zip (13 messages, latest: Sep 22 2022 at 05:09)
- Formal Series (5 messages, latest: Sep 22 2022 at 01:14)
- β Morphisms of quivers (3 messages, latest: Sep 21 2022 at 09:52)
- more picard_lindelof (14 messages, latest: Sep 21 2022 at 03:09)
- ideal.nat_cast (22 messages, latest: Sep 20 2022 at 12:23)
- Cauchy sequences are totally bounded (4 messages, latest: Sep 20 2022 at 05:13)
- finset from a finite subset of an infinite set (23 messages, latest: Sep 17 2022 at 13:06)
- Constant functions are analytic (6 messages, latest: Sep 16 2022 at 17:28)
- Formal verification of LLVM? (14 messages, latest: Sep 15 2022 at 13:17)
- real complex smul_comm_class (13 messages, latest: Sep 14 2022 at 23:50)
- Order on
fin n.succ
(21 messages, latest: Sep 14 2022 at 10:51) - or.elim_left/right (9 messages, latest: Sep 14 2022 at 10:38)
- Nested intervals (4 messages, latest: Sep 14 2022 at 03:59)
- 1/2 is not an integer (18 messages, latest: Sep 13 2022 at 22:32)
- β Taylor series (2 messages, latest: Sep 13 2022 at 16:03)
- Prop as
canonically_ordered_monoid
(12 messages, latest: Sep 13 2022 at 15:47) - is_open_set_of_eventually_nhds_within (5 messages, latest: Sep 13 2022 at 13:10)
- Integrability of powers of norm (16 messages, latest: Sep 13 2022 at 05:44)
- Sum over characteristic function (40 messages, latest: Sep 12 2022 at 23:10)
- fin.range (2 messages, latest: Sep 12 2022 at 17:15)
- Taylor series (7 messages, latest: Sep 12 2022 at 13:49)
- canonically_linear_ordered_monoid.to_linear_ordered_comm_β¦ (1 message, latest: Sep 11 2022 at 21:24)
- β converse of
nat.sub_le_sub_left
(13 messages, latest: Sep 11 2022 at 18:08) - Finite cyclic graphs (7 messages, latest: Sep 11 2022 at 17:39)
- Lists (5 messages, latest: Sep 09 2022 at 23:38)
- Pseudometric def of uniform space (26 messages, latest: Sep 08 2022 at 21:00)
- β Product of locally finite simple graphs (15 messages, latest: Sep 08 2022 at 14:22)
canonically_ordered_monoid
not inhabited? (8 messages, latest: Sep 08 2022 at 13:09)- β Binomial coefficients (2 messages, latest: Sep 08 2022 at 08:28)
- Binomial coefficients (3 messages, latest: Sep 08 2022 at 08:08)
- Product of locally finite simple graphs (5 messages, latest: Sep 08 2022 at 07:37)
- bit0/bit1 and mod (9 messages, latest: Sep 06 2022 at 10:31)
- Properties of products (56 messages, latest: Sep 02 2022 at 17:51)
- injective + mul bundling (4 messages, latest: Sep 01 2022 at 20:52)
- Monoidal functor from preserves limits/colimits (1 message, latest: Sep 01 2022 at 17:39)
- unique products (65 messages, latest: Sep 01 2022 at 12:19)
- .inj (6 messages, latest: Sep 01 2022 at 07:47)
- Constraints on lambda function (22 messages, latest: Aug 31 2022 at 21:48)
- Can't infer nontrivial β (16 messages, latest: Aug 31 2022 at 19:05)
- Largest element satisfying P in range (4 messages, latest: Aug 31 2022 at 16:10)
- normed structures on quotients (20 messages, latest: Aug 31 2022 at 13:32)
- is_regular.inj (22 messages, latest: Aug 30 2022 at 19:43)
- Continuity and inducing (4 messages, latest: Aug 30 2022 at 07:28)
- Sorting is injective (6 messages, latest: Aug 30 2022 at 07:07)
- A tactic for "reaching" inside a quantified statement? (5 messages, latest: Aug 29 2022 at 23:47)
- ext for linear maps from a tensor product (7 messages, latest: Aug 28 2022 at 21:20)
- order of one in zmod (13 messages, latest: Aug 28 2022 at 06:32)
- cardinal.le_of_add_le_add (14 messages, latest: Aug 26 2022 at 15:18)
- Fin k -> Fin (k + n) (2 messages, latest: Aug 26 2022 at 10:13)
- Moore-Smith sequences (7 messages, latest: Aug 25 2022 at 17:23)
- restricted set of equality points is closed (10 messages, latest: Aug 24 2022 at 14:56)
- computable finset to list (3 messages, latest: Aug 24 2022 at 05:21)
- Composing finite number of morphisms? (5 messages, latest: Aug 24 2022 at 03:20)
- Subfunctors (16 messages, latest: Aug 23 2022 at 16:40)
- Decomposition of the symmetry group of euclidean space (3 messages, latest: Aug 23 2022 at 06:12)
- Factoring zero roots (20 messages, latest: Aug 22 2022 at 08:57)
- suprβ_add (5 messages, latest: Aug 21 2022 at 23:23)
- β Prop structure equivalent to its components? (8 messages, latest: Aug 21 2022 at 22:51)
- open interval (14 messages, latest: Aug 21 2022 at 11:20)
- β integrability under translation (2 messages, latest: Aug 21 2022 at 09:51)
- integrability under translation (4 messages, latest: Aug 21 2022 at 05:57)
- model finding (11 messages, latest: Aug 19 2022 at 20:23)
- Real as limit of sequence of rationals (38 messages, latest: Aug 19 2022 at 00:00)
- Discrete subgroup of Hausdorff group is closed (18 messages, latest: Aug 18 2022 at 14:56)
- ne_zero without mul_zero_class (3 messages, latest: Aug 18 2022 at 14:17)
- β forallβ nth_le (2 messages, latest: Aug 17 2022 at 23:01)
- smul_mem_class (2 messages, latest: Aug 17 2022 at 21:54)
- β set Ξ± in fintype Ξ± (5 messages, latest: Aug 17 2022 at 14:57)
- nat.exists_eq_supr (5 messages, latest: Aug 17 2022 at 08:23)
- meet-irreducible element (4 messages, latest: Aug 17 2022 at 07:59)
- universal morphism in category theory (2 messages, latest: Aug 17 2022 at 04:36)
- pointwise ops on nhds (6 messages, latest: Aug 16 2022 at 17:22)
- opening the square (14 messages, latest: Aug 16 2022 at 17:11)
- check all the cases mod 4 (5 messages, latest: Aug 16 2022 at 13:31)
- forallβ nth_le (25 messages, latest: Aug 16 2022 at 13:25)
- β limit of a nonnegative sequence is nonnegative (4 messages, latest: Aug 16 2022 at 04:25)
- β natural transformation horizontal composition (1 message, latest: Aug 14 2022 at 17:52)
- natural transformation horizontal composition (3 messages, latest: Aug 14 2022 at 15:23)
- Continuous complex ring hom (17 messages, latest: Aug 14 2022 at 12:32)
- continuity of continuous composition (44 messages, latest: Aug 12 2022 at 12:32)
- is_open_bInter_finset (14 messages, latest: Aug 12 2022 at 12:18)
- checking a proof uses all its assumptions (38 messages, latest: Aug 12 2022 at 08:33)
- list.sorted with list.map? (2 messages, latest: Aug 12 2022 at 06:30)
- f x = 1 for subsingletons (2 messages, latest: Aug 11 2022 at 17:03)
- countably infinite type β β (4 messages, latest: Aug 11 2022 at 07:29)
- β β (x : β), is_algebraic β x β is_algebraic β€ x (3 messages, latest: Aug 11 2022 at 03:05)
- filtering a (finite) group to a subgroup (12 messages, latest: Aug 11 2022 at 01:01)
- β sub one succ (1 message, latest: Aug 10 2022 at 23:13)
- sub one succ (2 messages, latest: Aug 10 2022 at 23:13)
- Multinomial theorem (3 messages, latest: Aug 10 2022 at 20:55)
- linear order on finsupps (35 messages, latest: Aug 10 2022 at 18:29)
- ennreal.supr_coe (12 messages, latest: Aug 10 2022 at 14:42)
- more linear algebra (5 messages, latest: Aug 10 2022 at 14:34)
- How to prove well-founded recursion (3 messages, latest: Aug 10 2022 at 01:13)
- BanachβAlaoglu theorem (37 messages, latest: Aug 09 2022 at 19:55)
- metric bounded for normed space (4 messages, latest: Aug 09 2022 at 15:51)
- module.free β (fin 2 β β) (10 messages, latest: Aug 09 2022 at 13:02)
- β (x : β), is_algebraic β x β is_algebraic β€ x (2 messages, latest: Aug 09 2022 at 09:34)
- some linear algebra (28 messages, latest: Aug 09 2022 at 05:54)
- squares equal iff args are (19 messages, latest: Aug 08 2022 at 23:50)
- β Repeated Function Composition (2 messages, latest: Aug 08 2022 at 23:34)
- Repeated Function Composition (4 messages, latest: Aug 08 2022 at 22:36)
- β a % (b * c) % c = a % c (1 message, latest: Aug 08 2022 at 17:41)
fdifferential
totangent_space
(2 messages, latest: Aug 08 2022 at 08:01)- a % (b * c) % c = a % c (3 messages, latest: Aug 07 2022 at 20:38)
- Trivial ite lemma (19 messages, latest: Aug 07 2022 at 17:21)
- the "augmentation ideal" of a multivariable polynomial ring (5 messages, latest: Aug 06 2022 at 23:02)
- is_limit for an object (11 messages, latest: Aug 06 2022 at 15:42)
- matrix groups and Lie groups (43 messages, latest: Aug 05 2022 at 23:15)
- β function equivalence (4 messages, latest: Aug 05 2022 at 12:14)
- continuous_linear_map.eval (9 messages, latest: Aug 05 2022 at 05:14)
- β Ultrafilter convergence theorem? (4 messages, latest: Aug 04 2022 at 14:43)
- Raising absolute values to powers (9 messages, latest: Aug 04 2022 at 05:57)
- β mul_lt_left (5 messages, latest: Aug 04 2022 at 00:58)
- continuity of extension to completion (1 message, latest: Aug 03 2022 at 23:26)
- Restriction of a sum ignoring zeros (6 messages, latest: Aug 03 2022 at 20:17)
- equation in β to equation in zmod n (27 messages, latest: Aug 03 2022 at 19:00)
- β equation in β to equation in zmod n (7 messages, latest: Aug 03 2022 at 14:45)
- β Cardinality for set of a fintype (9 messages, latest: Aug 03 2022 at 07:34)
- β Fubini for finite sums (4 messages, latest: Aug 03 2022 at 03:06)
exists_monic_map_eq_of_mem_range
(12 messages, latest: Aug 02 2022 at 17:55)- Existence from almost always and non-zero measure (8 messages, latest: Aug 02 2022 at 10:31)
- absolute value and complex conjugate (10 messages, latest: Aug 02 2022 at 02:32)
- β complex.cos ΞΈ = real.cos ΞΈ (3 messages, latest: Aug 01 2022 at 19:42)
- β splitting field as an
intermediate_field
(15 messages, latest: Aug 01 2022 at 17:56) - cos x = 1/2 β β¦ (2 messages, latest: Aug 01 2022 at 00:31)
- β c β set.Icc a b β (d * c) β set.Icc (d * a) (d * b) (3 messages, latest: Jul 31 2022 at 21:54)
- x β {y, z} β (x = y β¨ x = z) (19 messages, latest: Jul 31 2022 at 21:35)
- β Intersection of a chain of nonempty finsets is nonempty. (33 messages, latest: Jul 31 2022 at 21:07)
- c β set.Icc a b β (d * c) β set.Icc (d * a) (d * b) (6 messages, latest: Jul 31 2022 at 20:46)
- β judging for the same constructor (2 messages, latest: Jul 31 2022 at 15:12)
- judging for the same constructor (1 message, latest: Jul 31 2022 at 05:07)
- Niven's theorem (4 messages, latest: Jul 30 2022 at 22:39)
- bundled surjective function (8 messages, latest: Jul 30 2022 at 17:21)
- Intersection of a chain of nonempty finsets is nonempty. (6 messages, latest: Jul 30 2022 at 09:52)
- Elements of completion as limits (23 messages, latest: Jul 30 2022 at 04:28)
- continuity of sums (3 messages, latest: Jul 29 2022 at 16:20)
- Stabilizer of a set (3 messages, latest: Jul 29 2022 at 13:09)
- concrete matrix multiplication (38 messages, latest: Jul 29 2022 at 09:41)
- products over
(fin n)
(26 messages, latest: Jul 28 2022 at 21:17) - tendsto equivalent to is bounded (39 messages, latest: Jul 28 2022 at 20:26)
- |x|<epsilon for all epsilon (5 messages, latest: Jul 28 2022 at 16:29)
- Zippers (2 messages, latest: Jul 27 2022 at 21:51)
- Sorting by function value (17 messages, latest: Jul 27 2022 at 17:31)
- β list.nth_le and list.nth (2 messages, latest: Jul 27 2022 at 15:39)
- list.nth_le and list.nth (19 messages, latest: Jul 27 2022 at 13:48)
- β numpy/jax etc? (4 messages, latest: Jul 27 2022 at 02:47)
- tensor product distributes over
prod
(13 messages, latest: Jul 26 2022 at 04:03) - explicit sums (34 messages, latest: Jul 25 2022 at 16:14)
- β nat_degree of p + C a (5 messages, latest: Jul 22 2022 at 10:06)
- repr of reals (10 messages, latest: Jul 22 2022 at 03:24)
- non-unital subrings (6 messages, latest: Jul 21 2022 at 17:51)
- Multiplying sparse infinite matricies. (7 messages, latest: Jul 21 2022 at 14:14)
- Point close to the frontier (4 messages, latest: Jul 21 2022 at 09:41)
- Convergent sequences (16 messages, latest: Jul 21 2022 at 01:39)
- Planar geometry with Cartesian coordinates (60 messages, latest: Jul 20 2022 at 21:02)
- list equivalence relation (12 messages, latest: Jul 20 2022 at 20:25)
- submonoid.map_closure (3 messages, latest: Jul 20 2022 at 12:37)
- Induced subgraphs (30 messages, latest: Jul 19 2022 at 18:34)
- exists and forall in subsingleton (5 messages, latest: Jul 19 2022 at 15:08)
- Closest point on a line to a point not on it (18 messages, latest: Jul 19 2022 at 03:31)
- Bifunctor whiskering (23 messages, latest: Jul 19 2022 at 00:47)
- Local minimum of a function from second derivative (6 messages, latest: Jul 18 2022 at 19:54)
- add_tsub_add_le_tsub_add_tsub (9 messages, latest: Jul 18 2022 at 15:53)
- finset.sum eq sum over support (3 messages, latest: Jul 17 2022 at 15:51)
- induction on finite set (10 messages, latest: Jul 17 2022 at 07:53)
- β pairwise (β ) of pairwise (<) (3 messages, latest: Jul 17 2022 at 01:03)
- β is_localization.mk'_pow (2 messages, latest: Jul 15 2022 at 16:38)
- is_localization.mk'_pow (2 messages, latest: Jul 15 2022 at 15:47)
- Filter on (set X) (5 messages, latest: Jul 15 2022 at 07:05)
- Embedding is local (22 messages, latest: Jul 14 2022 at 17:26)
- Initial segment (3 messages, latest: Jul 14 2022 at 16:15)
- sum.lex and prod.lex as rel_embeddings (19 messages, latest: Jul 14 2022 at 16:07)
- to_list_map_prod (34 messages, latest: Jul 14 2022 at 11:51)
- inner product space eq (6 messages, latest: Jul 14 2022 at 06:27)
- downward-closedness under a general relation (24 messages, latest: Jul 14 2022 at 03:40)
- β Image equals image after surjection (3 messages, latest: Jul 13 2022 at 20:54)
- Image equals image after surjection (2 messages, latest: Jul 13 2022 at 18:00)
- cyclic ring (31 messages, latest: Jul 13 2022 at 14:06)
- Equivariant Functions (10 messages, latest: Jul 13 2022 at 12:30)
- tsum stretcher, adding zeroes to sums like this (10 messages, latest: Jul 13 2022 at 08:40)
with_bot.neg
(36 messages, latest: Jul 13 2022 at 05:04)- lemma exp_pi_mul_I_half : exp (βreal.pi * I / 2) = I := (2 messages, latest: Jul 13 2022 at 02:55)
- Splitting a complex summable tsum into real and imaginary (11 messages, latest: Jul 12 2022 at 22:40)
- tensor product of two A-algebras (6 messages, latest: Jul 12 2022 at 22:32)
- subsingleton (R ββ[R] A) (11 messages, latest: Jul 12 2022 at 16:30)
- Scalar multiplication on the right (9 messages, latest: Jul 12 2022 at 13:28)
- Extending intervals (13 messages, latest: Jul 12 2022 at 13:27)
- Sheafification section is amalgamation (8 messages, latest: Jul 12 2022 at 13:15)
- symmetric.on (4 messages, latest: Jul 12 2022 at 13:11)
- limsup_antitone_continuous_eq_antitone_continuous_liminf (11 messages, latest: Jul 11 2022 at 19:37)
- Euler's Formula (4 messages, latest: Jul 10 2022 at 20:48)
- Counting divisible by p (3 messages, latest: Jul 10 2022 at 17:00)
max_eq_max'
(6 messages, latest: Jul 09 2022 at 20:14)- finsupp from input/output pairs (22 messages, latest: Jul 09 2022 at 15:59)
- Exterior Differential Systems (8 messages, latest: Jul 09 2022 at 12:18)
- Matrix invertible if row lin. independent (2 messages, latest: Jul 09 2022 at 08:44)
- Neighborhoods of sets (13 messages, latest: Jul 08 2022 at 14:17)
- coe and option (22 messages, latest: Jul 08 2022 at 13:18)
- order isomorphism between β and β+ (3 messages, latest: Jul 08 2022 at 08:19)
- has_smul β k for field k (7 messages, latest: Jul 08 2022 at 07:56)
- rel_iso (<) (<) from order_iso (2 messages, latest: Jul 08 2022 at 04:13)
- definition of exp using tsum (13 messages, latest: Jul 08 2022 at 02:56)
- module.prod (18 messages, latest: Jul 07 2022 at 23:53)
- vector space (6 messages, latest: Jul 07 2022 at 21:10)
- Diagonal from a function (3 messages, latest: Jul 07 2022 at 17:49)
- nat.succ as an embedding (14 messages, latest: Jul 07 2022 at 16:34)
- Exponential of reals are real - as a subset of complex (3 messages, latest: Jul 07 2022 at 02:52)
- tactics to prove an equality of reals (3 messages, latest: Jul 05 2022 at 21:04)
- Limit of addition of functions (4 messages, latest: Jul 05 2022 at 16:08)
- Subalgebra to subring (8 messages, latest: Jul 04 2022 at 23:07)
- equivalent to zify for rationals (9 messages, latest: Jul 04 2022 at 05:08)
- pointwise conj_act on normal subgroups (4 messages, latest: Jul 03 2022 at 22:56)
- division algorithm (17 messages, latest: Jul 03 2022 at 18:24)
- Cayley-Hamilton theorem (22 messages, latest: Jul 03 2022 at 12:52)
- Open interval is open (3 messages, latest: Jul 02 2022 at 20:57)
- Sum is in span (14 messages, latest: Jul 02 2022 at 15:48)
- adjoin finset is number field (7 messages, latest: Jul 02 2022 at 06:36)
- canonical isomorphism between localizations (10 messages, latest: Jul 01 2022 at 08:57)
- fin (s.card) finset equiv (76 messages, latest: Jul 01 2022 at 07:26)
- induced/coinduced topology for a family of maps (3 messages, latest: Jun 30 2022 at 22:13)
- Coding theory and code-based crypography (72 messages, latest: Jun 30 2022 at 14:22)
- coercion from Z to R (2 messages, latest: Jun 30 2022 at 05:14)
- Two induction principles (9 messages, latest: Jun 29 2022 at 21:29)
- Scalar multiplication on functions (7 messages, latest: Jun 28 2022 at 16:40)
dite (h : P β§ Q)
andsplit_ifs
(4 messages, latest: Jun 28 2022 at 15:11)- Hyperbolic Geometry (12 messages, latest: Jun 28 2022 at 11:58)
additive
of subgroup (3 messages, latest: Jun 28 2022 at 11:05)- Algebraic Conjugate over Finite Fields (68 messages, latest: Jun 28 2022 at 03:39)
- β function with singleton support (5 messages, latest: Jun 28 2022 at 00:50)
- Graph Theory (159 messages, latest: Jun 27 2022 at 19:25)
- exists iff exists (4 messages, latest: Jun 27 2022 at 15:20)
- β
field_simp
for units (7 messages, latest: Jun 27 2022 at 13:16) - Finite chain has a maximal element (6 messages, latest: Jun 27 2022 at 12:58)
- determinant via exterior algebra (117 messages, latest: Jun 26 2022 at 21:31)
- Decidability of
is_unit
on finite rings (35 messages, latest: Jun 26 2022 at 20:15) - Length of longest chain (9 messages, latest: Jun 26 2022 at 16:20)
- Lie bracket, algebraic version (3 messages, latest: Jun 26 2022 at 03:07)
- Sesquilinear form (6 messages, latest: Jun 25 2022 at 23:41)
field_simp
for units (39 messages, latest: Jun 24 2022 at 15:25)- is_empty β₯s (3 messages, latest: Jun 24 2022 at 05:36)
- Arithmetic function and general functions (12 messages, latest: Jun 23 2022 at 17:41)
- List of expressions to expression for that list (8 messages, latest: Jun 22 2022 at 20:48)
- Infinite product (8 messages, latest: Jun 22 2022 at 19:16)
- β equivalence between multiple well-founded relation defiβ¦ (4 messages, latest: Jun 22 2022 at 17:16)
- β subgraphs (2 messages, latest: Jun 22 2022 at 08:56)
- "Projecting" a sigma type (4 messages, latest: Jun 22 2022 at 08:41)
- multiplicity of root in extension field (14 messages, latest: Jun 22 2022 at 05:52)
- subgraphs (18 messages, latest: Jun 21 2022 at 17:01)
- β multiset.prod = list.prod (4 messages, latest: Jun 21 2022 at 16:35)
- Convex hull membership (4 messages, latest: Jun 20 2022 at 16:06)
- β map (succ : β β β) at_top = at_top (6 messages, latest: Jun 20 2022 at 12:04)
- Uniform discreteness and relative density (1 message, latest: Jun 20 2022 at 11:03)
- Set is a submodule (3 messages, latest: Jun 20 2022 at 10:36)
- finset Ξ± β set Ξ± (17 messages, latest: Jun 20 2022 at 07:56)
- powers of an endofunctor (1 message, latest: Jun 20 2022 at 06:52)
- Composition of convex functions (2 messages, latest: Jun 19 2022 at 22:50)
- rat.cast_sum (7 messages, latest: Jun 19 2022 at 16:44)
- bijection (7 messages, latest: Jun 19 2022 at 02:22)
- Gcd of a set of natural numbers or integers (4 messages, latest: Jun 17 2022 at 19:37)
- Pullback well-foundedness (3 messages, latest: Jun 17 2022 at 17:13)
- β Specific integrals (2 messages, latest: Jun 17 2022 at 07:14)
- Specific integrals (1 message, latest: Jun 17 2022 at 07:13)
- Fixed point (6 messages, latest: Jun 16 2022 at 22:19)
- locally_constant_on (7 messages, latest: Jun 16 2022 at 17:38)
- In a trivial monoid, everything is a unit (37 messages, latest: Jun 16 2022 at 14:23)
- Restriction of
monoid_hom
to units? (8 messages, latest: Jun 16 2022 at 13:54) - Computing nat_degrees of polynomials (38 messages, latest: Jun 16 2022 at 08:01)
- First isomorphism theorem for abelian categories (2 messages, latest: Jun 16 2022 at 07:28)
- category-theoretic triviality (11 messages, latest: Jun 16 2022 at 01:47)
- Indeterminate Integral (13 messages, latest: Jun 15 2022 at 17:49)
- div by p_adic_val_nat is coprime (19 messages, latest: Jun 15 2022 at 15:12)
- Normalizing a vector (10 messages, latest: Jun 15 2022 at 11:19)
- β Explicit zeta and beta reductions (5 messages, latest: Jun 14 2022 at 21:31)
- Explicit zeta and beta reductions (2 messages, latest: Jun 14 2022 at 19:15)
- is_atomistic submodule (13 messages, latest: Jun 14 2022 at 18:10)
- Inserting into
is_scalar_tower
(11 messages, latest: Jun 13 2022 at 22:25) - category theory: isomorphisms between images (16 messages, latest: Jun 11 2022 at 09:34)
- Dimension of an affine space (14 messages, latest: Jun 10 2022 at 22:05)
- When does a functor preserve finite (co)limits? (4 messages, latest: Jun 10 2022 at 18:56)
direct_sum
andsum
(2 messages, latest: Jun 10 2022 at 14:51)- Making
finset.sum
into an explicit sum (20 messages, latest: Jun 09 2022 at 09:59) - Equiv version of
function.swap
(7 messages, latest: Jun 09 2022 at 07:37) - Definitional equality (37 messages, latest: Jun 08 2022 at 01:45)
- β Symmetric group? (4 messages, latest: Jun 07 2022 at 20:23)
- Stacking matrices (5 messages, latest: Jun 06 2022 at 19:13)
- epi_of_comp_epi_of_mono (11 messages, latest: Jun 05 2022 at 11:54)
- β multiset equivalent of is_absolute_value.abv_sum (1 message, latest: Jun 04 2022 at 14:26)
- multiset equivalent of is_absolute_value.abv_sum (3 messages, latest: Jun 04 2022 at 12:52)
- β fin.next (1 message, latest: Jun 03 2022 at 18:00)
- β cases on fin 1 (11 messages, latest: Jun 03 2022 at 14:16)
- div_mul_div_comm for nat (9 messages, latest: Jun 03 2022 at 11:25)
- A functor is additive iff⦠(2 messages, latest: Jun 02 2022 at 19:19)
- Cyclotomic extensions of finite fields are finite (13 messages, latest: Jun 02 2022 at 07:33)
- cases on fin 1 (4 messages, latest: Jun 02 2022 at 03:43)
- Statements about finite rings (15 messages, latest: Jun 01 2022 at 15:59)
- Standard basis (7 messages, latest: Jun 01 2022 at 14:34)
- Existence of elements of order p in a group (29 messages, latest: May 31 2022 at 07:22)
- false_of_lt_of_lt (3 messages, latest: May 30 2022 at 17:30)
- equivalence of two definitions of span (9 messages, latest: May 30 2022 at 16:17)
- cancelling an isomorphism in a concrete abelian category (1 message, latest: May 30 2022 at 12:26)
- β proof refiner (2 messages, latest: May 30 2022 at 03:34)
multiset.prod_congr
(1 message, latest: May 30 2022 at 01:52)- Relation between the integral of a function and derivative (21 messages, latest: May 29 2022 at 23:12)
- β Set of subsets of
t
is equivalent toset t
(1 message, latest: May 29 2022 at 21:20) - Set of subsets of
t
is equivalent toset t
(19 messages, latest: May 29 2022 at 21:00) - proof refiner (7 messages, latest: May 29 2022 at 19:03)
- β cycle.next and list.next (1 message, latest: May 28 2022 at 22:44)
- cycle.next and list.next (3 messages, latest: May 28 2022 at 21:37)
- β square root of 1 (15 messages, latest: May 28 2022 at 18:24)
- Weak dual with discrete topology (8 messages, latest: May 26 2022 at 19:43)
- β simple(?) summable lemma (4 messages, latest: May 26 2022 at 18:35)
- has_sum for consecutive reciprocals (5 messages, latest: May 26 2022 at 00:33)
- Semiconjugate matrices (17 messages, latest: May 25 2022 at 20:21)
- Lemmas about nat / list / finset (28 messages, latest: May 25 2022 at 00:06)
- nat powers of probabilities (22 messages, latest: May 23 2022 at 23:48)
- Structure theorem for finite(ly generated) abelian groups? (9 messages, latest: May 23 2022 at 16:34)
(fin (n + 1) β Ξ²) β Ξ² Γ (fin n β Ξ²)
(8 messages, latest: May 23 2022 at 11:39)- β Regular expression reversal (4 messages, latest: May 23 2022 at 10:06)
- Similarities (36 messages, latest: May 23 2022 at 00:06)
- Extensions of finite fields are Galois? (7 messages, latest: May 22 2022 at 13:51)
- The
n
th cyclotomic field has a prim.n
th root of unity (13 messages, latest: May 21 2022 at 19:08) - multiplication by a unit is injective (9 messages, latest: May 20 2022 at 22:23)
- closed graph theorem (15 messages, latest: May 20 2022 at 16:56)
- isolated zeros (2 messages, latest: May 19 2022 at 23:15)
- Riesz-Markov-Kakutani representation theorem (2 messages, latest: May 19 2022 at 22:52)
- β Shifting sums (2 messages, latest: May 19 2022 at 11:14)
- Shifting sums (5 messages, latest: May 19 2022 at 09:35)
- preorder on ulift (45 messages, latest: May 18 2022 at 18:06)
- finset proof (22 messages, latest: May 18 2022 at 02:57)
- Discrete Fourier transform (20 messages, latest: May 17 2022 at 23:09)
- set equality (9 messages, latest: May 17 2022 at 16:50)
- Working on the projective line (24 messages, latest: May 16 2022 at 16:40)
- dot_product as inner_product_space (5 messages, latest: May 15 2022 at 20:45)
- Basic set_of lemmas (3 messages, latest: May 15 2022 at 19:31)
- ite_then_ite (16 messages, latest: May 14 2022 at 13:33)
- finset semiring (22 messages, latest: May 13 2022 at 09:44)
- (in)finite binary trees (4 messages, latest: May 12 2022 at 18:29)
- double categories (6 messages, latest: May 12 2022 at 14:09)
- monotone convergence for real sequences (3 messages, latest: May 11 2022 at 20:12)
- Finite field extensions (7 messages, latest: May 10 2022 at 11:09)
- Simpler proof of injectivity {0,1,-1} β> R? (15 messages, latest: May 10 2022 at 10:19)
- β degree of a polynomial (13 messages, latest: May 09 2022 at 11:52)
- equiv_embedding_image (4 messages, latest: May 09 2022 at 11:44)
- coercion into algebraic closure? (28 messages, latest: May 09 2022 at 09:09)
- comp_assoc (5 messages, latest: May 09 2022 at 06:46)
- β using tendsto (11 messages, latest: May 08 2022 at 21:29)
- β prime factorisation (7 messages, latest: May 08 2022 at 20:36)
- using tendsto (7 messages, latest: May 08 2022 at 20:09)
- Riemann Mapping Theorem (10 messages, latest: May 08 2022 at 19:00)
- prime factorisation (7 messages, latest: May 08 2022 at 18:30)
- multiplicity_gcd (9 messages, latest: May 08 2022 at 16:24)
- Why are there two transitive closures? (20 messages, latest: May 08 2022 at 07:19)
- β Lean equivalent to Coq programs? (10 messages, latest: May 08 2022 at 07:00)
- degree of a polynomial (8 messages, latest: May 07 2022 at 18:13)
- inv_of_inj (12 messages, latest: May 07 2022 at 17:15)
- simple function from finite restriction (4 messages, latest: May 06 2022 at 23:14)
- Lean equivalent to Coq programs? (13 messages, latest: May 06 2022 at 20:11)
- Hom-tensor adjunction? (10 messages, latest: May 06 2022 at 16:54)
- ae measurable condition (14 messages, latest: May 06 2022 at 13:29)
- Nonconstant holomorphic functions are open maps (7 messages, latest: May 06 2022 at 13:23)
- Special Linear Groups (16 messages, latest: May 06 2022 at 03:49)
- Currying smooth maps (1 message, latest: May 05 2022 at 13:32)
- is_atomic_of_well_founded (3 messages, latest: May 05 2022 at 06:32)
- Total variation distance on pmf (2 messages, latest: May 04 2022 at 20:22)
- algebra_map clm (6 messages, latest: May 04 2022 at 15:13)
- finsupp.nonzero_iff_exist (22 messages, latest: May 04 2022 at 12:49)
- log over rpow (10 messages, latest: May 03 2022 at 19:36)
- Injectivity of arrow type constructor (20 messages, latest: May 03 2022 at 18:30)
- limit of a sum over nat (10 messages, latest: May 03 2022 at 15:29)
- Endomorphism of ring over itself (4 messages, latest: May 03 2022 at 14:30)
- binary for
nnreal
(6 messages, latest: May 03 2022 at 00:16) - Tor (7 messages, latest: May 02 2022 at 18:06)
- β lcm_pos_pos (1 message, latest: May 02 2022 at 18:00)
- β Frobenius norm (10 messages, latest: May 02 2022 at 17:56)
- strictly between squares β> not a square? (13 messages, latest: May 02 2022 at 15:55)
- additive functors preserve binary biproducts (8 messages, latest: May 02 2022 at 15:12)
- monotone_on.mono (7 messages, latest: May 02 2022 at 07:43)
- matrices (24 messages, latest: May 02 2022 at 01:18)
- a fact about equivalences built fiber-wise (9 messages, latest: May 02 2022 at 00:03)
- set.card_to_finset_prod (7 messages, latest: May 01 2022 at 22:39)
- Relating the categorical product and the normal product (23 messages, latest: May 01 2022 at 11:47)
- a fact about cardinalities of preimages (1 message, latest: May 01 2022 at 07:58)
- β bijective function between types of equal cardinality (5 messages, latest: May 01 2022 at 01:38)
- bijective function between types of equal cardinality (7 messages, latest: May 01 2022 at 00:15)
- Does this theorem exist? (1 message, latest: Apr 30 2022 at 22:57)
- subrelation on more than one type (7 messages, latest: Apr 30 2022 at 20:32)
- β Understanding local context (7 messages, latest: Apr 30 2022 at 18:40)
- finset.sum (5 messages, latest: Apr 30 2022 at 11:05)
- linear_map congr (13 messages, latest: Apr 29 2022 at 16:08)
- Sum as integral (3 messages, latest: Apr 29 2022 at 12:28)
- finite_dimensional_of_injective (8 messages, latest: Apr 29 2022 at 10:22)
- Cauchy-Schwarz (22 messages, latest: Apr 29 2022 at 09:52)
- β Cantor's diagonal theorem (11 messages, latest: Apr 29 2022 at 00:51)
- s equiv s.to_finset (5 messages, latest: Apr 28 2022 at 10:15)
- Resultant (2 messages, latest: Apr 27 2022 at 15:16)
- sum of row sums equals sum of column sums (17 messages, latest: Apr 27 2022 at 11:57)
- Distributivity of ite (1 message, latest: Apr 27 2022 at 10:00)
- pi.nonempty (11 messages, latest: Apr 26 2022 at 23:45)
- Type-ascript to a Euclidean space (22 messages, latest: Apr 26 2022 at 16:31)
- Link to files (8 messages, latest: Apr 26 2022 at 13:13)
- representations of k-algebras (9 messages, latest: Apr 26 2022 at 13:07)
- making implicit variable explicit in output (20 messages, latest: Apr 26 2022 at 07:29)
- Finiteness of tensor product (7 messages, latest: Apr 26 2022 at 06:54)
- lintegral_coe_eq_coe_integral (7 messages, latest: Apr 25 2022 at 20:38)
- Zero-dimensional space (1 message, latest: Apr 25 2022 at 19:09)
- lcm_pos_pos (3 messages, latest: Apr 25 2022 at 17:05)
- maps_to_prod (3 messages, latest: Apr 25 2022 at 13:02)
- boundedness of sums (4 messages, latest: Apr 25 2022 at 10:41)
- PL theory stuff (3 messages, latest: Apr 24 2022 at 11:01)
- β Linear map from the base ring (1 message, latest: Apr 22 2022 at 13:40)
- add_min_max (5 messages, latest: Apr 22 2022 at 11:34)
- β mod_pow_mod (2 messages, latest: Apr 22 2022 at 09:38)
- Linear map from the base ring (5 messages, latest: Apr 22 2022 at 03:29)
- every finite type admits a linear order (10 messages, latest: Apr 21 2022 at 18:16)
- β Equip a type with the discrete topology (1 message, latest: Apr 21 2022 at 15:04)
- sum_ite_eq_extract (21 messages, latest: Apr 21 2022 at 14:49)
- Switch limit and derivative given uniform convergence (5 messages, latest: Apr 20 2022 at 18:05)
- mod_pow_mod (17 messages, latest: Apr 20 2022 at 15:25)
- Finset filter map (2 messages, latest: Apr 19 2022 at 20:00)
- arclength of a function (7 messages, latest: Apr 19 2022 at 18:56)
- ring.inverse is continuous (38 messages, latest: Apr 19 2022 at 14:40)
- Integers of norm at most one (18 messages, latest: Apr 19 2022 at 12:50)
- Trace of tensor product (2 messages, latest: Apr 19 2022 at 12:33)
- finset.sup_mul_left (24 messages, latest: Apr 19 2022 at 10:37)
- Localization of β€ at p as a subring of β with hom. to β€/pβ€? (30 messages, latest: Apr 19 2022 at 02:02)
- use tactic (21 messages, latest: Apr 18 2022 at 22:24)
- lcm and divisors (9 messages, latest: Apr 18 2022 at 08:35)
- filter mapβ as map (30 messages, latest: Apr 17 2022 at 21:43)
- set.any (10 messages, latest: Apr 17 2022 at 20:05)
- sum_sum (7 messages, latest: Apr 17 2022 at 15:15)
- β Product of sums as double sum? (3 messages, latest: Apr 16 2022 at 18:31)
- β inversion of a group with zero as a monoid_with_zero_hom? (2 messages, latest: Apr 16 2022 at 18:21)
- inversion of a group with zero as a monoid_with_zero_hom? (3 messages, latest: Apr 16 2022 at 18:14)
- β
not_not
+mt
(4 messages, latest: Apr 16 2022 at 16:40) - non-unital comm (semi)ring (7 messages, latest: Apr 16 2022 at 06:02)
- rat.mul_eq (3 messages, latest: Apr 15 2022 at 18:55)
- Elements of finite fields of char 2 are squares (13 messages, latest: Apr 15 2022 at 18:50)
- lcm equal first iff second divides first (8 messages, latest: Apr 15 2022 at 12:02)
- β Continuous linear map finite dimension (10 messages, latest: Apr 15 2022 at 10:17)
- β a - b = -b + a (11 messages, latest: Apr 15 2022 at 07:22)
- power of product in comm_monoid (4 messages, latest: Apr 14 2022 at 15:56)
- The "other kind" of commutator (7 messages, latest: Apr 14 2022 at 14:24)
- C(S, V) complete and separated (9 messages, latest: Apr 14 2022 at 14:11)
- Lp for 0<p<1 (17 messages, latest: Apr 14 2022 at 07:46)
- Localization inside of fraction field (3 messages, latest: Apr 13 2022 at 16:20)
- rat-normed space (8 messages, latest: Apr 13 2022 at 13:18)
- filter.has_scalar missing? (46 messages, latest: Apr 12 2022 at 23:19)
- bijection
range n β zmod n
? (152 messages, latest: Apr 12 2022 at 22:17) - A finite field has at least two elements (10 messages, latest: Apr 12 2022 at 18:30)
- square root of 1 (7 messages, latest: Apr 11 2022 at 20:21)
- β Find the nth element of an ordered finset (2 messages, latest: Apr 11 2022 at 13:25)
- Find the nth element of an ordered finset (6 messages, latest: Apr 11 2022 at 13:25)
- monoid_hom from mul_hom? (15 messages, latest: Apr 11 2022 at 13:07)
- coefficients of sum a(n) X^n (3 messages, latest: Apr 11 2022 at 04:03)
- Even power of -1 (16 messages, latest: Apr 09 2022 at 17:54)
- pfun to total function (11 messages, latest: Apr 09 2022 at 16:46)
- β Indicator of intersection (5 messages, latest: Apr 09 2022 at 14:33)
- Indicator of intersection (6 messages, latest: Apr 09 2022 at 12:03)
- Working with polynomial factorizations (132 messages, latest: Apr 09 2022 at 06:52)
- Sequence limit (4 messages, latest: Apr 08 2022 at 15:41)
- Tensor maps (15 messages, latest: Apr 08 2022 at 02:24)
- Finiteness of subalgebra of algebraic extensions of F_p (9 messages, latest: Apr 07 2022 at 15:09)
- Continuity of integral for a sub-sigma-field (10 messages, latest: Apr 07 2022 at 14:38)
- β a dependent version of finset.bUnion? (5 messages, latest: Apr 07 2022 at 12:08)
- traversing an expression making replacements (3 messages, latest: Apr 07 2022 at 09:04)
- ideal generator element of ideal (27 messages, latest: Apr 06 2022 at 20:13)
- appended lists equal of length equal (11 messages, latest: Apr 06 2022 at 15:02)
- Sequence density (2 messages, latest: Apr 06 2022 at 15:02)
- p-adic valuation (49 messages, latest: Apr 05 2022 at 20:34)
- lemma about when a filter is a pure filter (58 messages, latest: Apr 04 2022 at 17:04)
- a < b β§ a = b β false (4 messages, latest: Apr 04 2022 at 16:46)
- Finitary scalar product (36 messages, latest: Apr 04 2022 at 13:34)
- β Mapping into a finset product (6 messages, latest: Apr 03 2022 at 02:46)
- word length in a free group (8 messages, latest: Apr 01 2022 at 16:57)
- char_zero instance on polynomials (34 messages, latest: Mar 31 2022 at 15:55)
- Equip a type with the discrete topology (10 messages, latest: Mar 31 2022 at 10:04)
- β category of sheaf is abelian (26 messages, latest: Mar 31 2022 at 02:40)
- β equiv.cast that preserves structure (1 message, latest: Mar 30 2022 at 17:20)
- equiv.cast that preserves structure (8 messages, latest: Mar 30 2022 at 16:20)
- β Almost equal preimages (3 messages, latest: Mar 30 2022 at 15:12)
- β Prove known function is group isomorphism (3 messages, latest: Mar 30 2022 at 13:35)
- Prove known function is group isomorphism (3 messages, latest: Mar 30 2022 at 12:17)
- independent random variables (10 messages, latest: Mar 30 2022 at 09:40)
- β Preimage of normed ball (2 messages, latest: Mar 30 2022 at 09:22)
- Preimage of normed ball (11 messages, latest: Mar 30 2022 at 09:02)
- Abelian subgroup dividing order (5 messages, latest: Mar 30 2022 at 06:46)
- Determining Integral (11 messages, latest: Mar 30 2022 at 00:45)
- neg_zero for has_distrib_neg (7 messages, latest: Mar 29 2022 at 20:30)
- hom.op_inv (20 messages, latest: Mar 29 2022 at 19:48)
- nat.antidiagonal for pi types (16 messages, latest: Mar 29 2022 at 12:35)
- basis..sum_extend_extends (2 messages, latest: Mar 29 2022 at 10:22)
- num_3_dvd_of_mod_9_eq_3_or_6 (3 messages, latest: Mar 29 2022 at 07:52)
- Q is injective (3 messages, latest: Mar 28 2022 at 22:18)
- algebra β[X] R[X] (41 messages, latest: Mar 28 2022 at 10:13)
- Expressing xβ»ΒΉ from a polynomial equality (4 messages, latest: Mar 28 2022 at 09:32)
- Mapping into a finset product (15 messages, latest: Mar 27 2022 at 23:27)
- β Cartesian product in finset (1 message, latest: Mar 27 2022 at 22:28)
- Cartesian product in finset (6 messages, latest: Mar 27 2022 at 22:07)
- mixed version of ssubset_trans (14 messages, latest: Mar 27 2022 at 15:59)
- Stacks definition of abelian cats (43 messages, latest: Mar 27 2022 at 04:05)
- is_prime_field (13 messages, latest: Mar 26 2022 at 18:29)
- polynomial.comp_prod (27 messages, latest: Mar 26 2022 at 17:30)
- symmetric difference / disjunctive union of sets (47 messages, latest: Mar 26 2022 at 17:02)
- closure of element of infinite order (15 messages, latest: Mar 25 2022 at 17:14)
- Named deferred goals (11 messages, latest: Mar 25 2022 at 14:45)
- char_p instance on polynomials (5 messages, latest: Mar 25 2022 at 12:07)
- β Dimension of intersection (13 messages, latest: Mar 24 2022 at 20:10)
- polynomial preimage of nonzero is dense (19 messages, latest: Mar 24 2022 at 18:48)
- Bounded conditional supremum (44 messages, latest: Mar 24 2022 at 14:09)
- finsupp total eq sum (14 messages, latest: Mar 24 2022 at 09:15)
- groups of order pΒ² (5 messages, latest: Mar 23 2022 at 21:45)
- p-adic norm of (a : int) = 1 from p not dividing a? (14 messages, latest: Mar 23 2022 at 20:48)
- Independent iff independent (4 messages, latest: Mar 23 2022 at 08:17)
- sup metric convergence is uniform convergence (8 messages, latest: Mar 23 2022 at 04:18)
- Smallness from a cardinal bound (3 messages, latest: Mar 22 2022 at 20:36)
- more inductions for int (52 messages, latest: Mar 22 2022 at 18:36)
- hom from mul monoid to add monoid (4 messages, latest: Mar 22 2022 at 08:14)
- Applying continuous linear map (5 messages, latest: Mar 21 2022 at 21:31)
- β scaling of union (5 messages, latest: Mar 21 2022 at 16:52)
- multiplicity of derivative (12 messages, latest: Mar 21 2022 at 11:57)
- Partial derivatives' chain rule & product rule (3 messages, latest: Mar 21 2022 at 11:32)
- int.gcd_add_self_right (3 messages, latest: Mar 20 2022 at 23:07)
- filter.comapβ (4 messages, latest: Mar 20 2022 at 17:25)
- finding instance declaration (20 messages, latest: Mar 19 2022 at 21:25)
- finset of functions (4 messages, latest: Mar 19 2022 at 20:57)
- Totally boundedness (2 messages, latest: Mar 19 2022 at 15:44)
- Realizing the Hausdorff distance (19 messages, latest: Mar 19 2022 at 01:19)
- Splitting lemma for modules (7 messages, latest: Mar 18 2022 at 23:27)
- Reference a part of an expression (19 messages, latest: Mar 18 2022 at 23:26)
- nilpotency in finite groups (14 messages, latest: Mar 18 2022 at 22:54)
- β
emetric.continuous_at_iff
(2 messages, latest: Mar 18 2022 at 18:50) emetric.continuous_at_iff
(3 messages, latest: Mar 18 2022 at 16:46)- triangle equality if arg is equal (13 messages, latest: Mar 17 2022 at 23:43)
- β nat.lt_iff_eq_succ (6 messages, latest: Mar 16 2022 at 22:18)
- is_closed.smul for fields (12 messages, latest: Mar 16 2022 at 22:16)
- 2 is not a square (37 messages, latest: Mar 16 2022 at 08:02)
- tensor products commute with direct limits (57 messages, latest: Mar 16 2022 at 06:58)
- Integral of 1/sqrt(x) (24 messages, latest: Mar 16 2022 at 05:19)
- nat.lt_iff_eq_succ (5 messages, latest: Mar 15 2022 at 23:53)
- Hom(Z,A) (11 messages, latest: Mar 14 2022 at 23:09)
- stream events (2 messages, latest: Mar 14 2022 at 20:02)
- Coprimeness of products from pairwise coprimeness (16 messages, latest: Mar 14 2022 at 12:31)
- Functions into sums (32 messages, latest: Mar 14 2022 at 11:37)
- checking if function is a probability measure (8 messages, latest: Mar 13 2022 at 20:13)
- mkq = 0 iff (8 messages, latest: Mar 13 2022 at 08:13)
- β clearing denominators (1 message, latest: Mar 12 2022 at 20:13)
- clearing denominators (5 messages, latest: Mar 12 2022 at 20:13)
- transferring topological properties along homeomorphisms (16 messages, latest: Mar 12 2022 at 15:16)
- classes for symmetric transitive relation (22 messages, latest: Mar 11 2022 at 16:05)
- Injectivity of quiver.hom.op (5 messages, latest: Mar 11 2022 at 14:39)
- Injectivity of functor.op (10 messages, latest: Mar 11 2022 at 13:05)
- tendsto.units (3 messages, latest: Mar 10 2022 at 22:17)
- zmod.nat_cast_eq_iff (11 messages, latest: Mar 10 2022 at 17:43)
- linear_map.eq_locus (5 messages, latest: Mar 10 2022 at 17:42)
- β cartesian product (8 messages, latest: Mar 10 2022 at 15:37)
- cartesian product (5 messages, latest: Mar 10 2022 at 15:11)
- fin n with saturating addition (19 messages, latest: Mar 10 2022 at 13:20)
- polynomial.map as algebra hom (10 messages, latest: Mar 10 2022 at 13:05)
- nat abs or (2 messages, latest: Mar 10 2022 at 01:34)
- injection to show cardinality inquality (5 messages, latest: Mar 09 2022 at 22:34)
- A-B (14 messages, latest: Mar 09 2022 at 18:48)
- β equivalence of category preserves (co)limits (4 messages, latest: Mar 09 2022 at 12:50)
- Range equiv quotient by ker (7 messages, latest: Mar 09 2022 at 11:17)
- Power of two (22 messages, latest: Mar 08 2022 at 11:23)
- β nat_mul_comm (7 messages, latest: Mar 08 2022 at 10:54)
- β
nat.ceil
onnnreal
? (1 message, latest: Mar 07 2022 at 21:46) nat.ceil
onnnreal
? (26 messages, latest: Mar 07 2022 at 16:15)- unbounded function (1 message, latest: Mar 07 2022 at 15:08)
- Isometry group of pseudo_emetric space splits (1 message, latest: Mar 06 2022 at 09:36)
- Multiplicity in the naturals (29 messages, latest: Mar 05 2022 at 06:35)
geom_sum (X n)
is monic (11 messages, latest: Mar 04 2022 at 14:39)- summable.single_le_tsum (4 messages, latest: Mar 04 2022 at 14:07)
- Completeness of padics (25 messages, latest: Mar 03 2022 at 21:17)
- omega < aleph (n+1) (19 messages, latest: Mar 03 2022 at 19:53)
- cancel division in polynomials (8 messages, latest: Mar 02 2022 at 18:38)
- nnnorm and complex (3 messages, latest: Mar 02 2022 at 17:24)
- (Co)completion of a category (11 messages, latest: Mar 02 2022 at 15:54)
- C1 on product (5 messages, latest: Mar 02 2022 at 13:34)
- submodule.sup basic lemma (9 messages, latest: Mar 02 2022 at 10:44)
- β prod.fst as a hom (3 messages, latest: Mar 01 2022 at 21:05)
- int.to_nat_eq_zero (8 messages, latest: Mar 01 2022 at 20:17)
- β Creating a example
perm
(1 message, latest: Mar 01 2022 at 19:36) - undergrad todo trivial target Linear Algebra / Duality / (5 messages, latest: Mar 01 2022 at 18:58)
- computable operations for rational numbers (8 messages, latest: Mar 01 2022 at 18:44)
- difference of squares of commuting elements (7 messages, latest: Mar 01 2022 at 12:04)
- universal property of sheafification (on topological spaces) (15 messages, latest: Mar 01 2022 at 10:57)
- Completeness of direct sums of Hilbert spaces? (4 messages, latest: Mar 01 2022 at 03:45)
- Creating a example
perm
(3 messages, latest: Mar 01 2022 at 00:41) - topological embeddings of orders (2 messages, latest: Feb 28 2022 at 17:12)
- subtype.coe_fn_coe (4 messages, latest: Feb 28 2022 at 13:09)
- the law of a random variable is a probability measure (17 messages, latest: Feb 28 2022 at 02:24)
- S - {x} ? (8 messages, latest: Feb 27 2022 at 20:38)
- Bump functions (32 messages, latest: Feb 27 2022 at 20:22)
- β List repeat (4 messages, latest: Feb 27 2022 at 18:06)
- List repeat (3 messages, latest: Feb 27 2022 at 15:18)
- Group Amalgamation (2 messages, latest: Feb 26 2022 at 21:49)
- base change / pullback (10 messages, latest: Feb 26 2022 at 12:10)
- set.sigma (8 messages, latest: Feb 26 2022 at 11:04)
- finset.sum_add (4 messages, latest: Feb 26 2022 at 08:09)
- submodule of free module over PID is free (15 messages, latest: Feb 25 2022 at 16:28)
ring_equiv.Pi_congr_right
(4 messages, latest: Feb 25 2022 at 16:11)- Minimal polynomial of
ΞΆ - 1
(2 messages, latest: Feb 25 2022 at 12:12) - Finite types (6 messages, latest: Feb 25 2022 at 11:48)
- Frobenius norm (1 message, latest: Feb 24 2022 at 22:52)
- β Ξ΄-Ι continuity for metric spaces (11 messages, latest: Feb 24 2022 at 22:36)
- Ξ΄-Ι continuity for metric spaces (1 message, latest: Feb 24 2022 at 22:02)
- with_zero (multiplicative A) β* multiplicative (with_bot A) (32 messages, latest: Feb 24 2022 at 20:01)
- units as a functor (8 messages, latest: Feb 24 2022 at 09:48)
- Ξ± β Ξ² β option Ξ± β option Ξ² (3 messages, latest: Feb 24 2022 at 00:35)
- exists_extends of linear_pmap (18 messages, latest: Feb 23 2022 at 21:26)
- Continuous algebra homomorphisms (37 messages, latest: Feb 22 2022 at 19:25)
- continuous bilinear map (14 messages, latest: Feb 22 2022 at 13:21)
- is_iso dist triang (17 messages, latest: Feb 22 2022 at 00:42)
- β nat pow tendsto (3 messages, latest: Feb 22 2022 at 00:01)
- nat pow tendsto (3 messages, latest: Feb 21 2022 at 22:28)
- cokernel_lift_iso_kernel_desc (31 messages, latest: Feb 21 2022 at 21:08)
- At least three elements (28 messages, latest: Feb 21 2022 at 20:06)
- apply function n times (47 messages, latest: Feb 20 2022 at 18:11)
- set to list (16 messages, latest: Feb 20 2022 at 01:32)
- completion of a normed space (14 messages, latest: Feb 19 2022 at 17:39)
- β Lagrange's Theorem (Group theory) (10 messages, latest: Feb 19 2022 at 01:19)
- nnnorm and int.nat_abs (11 messages, latest: Feb 18 2022 at 08:48)
- finset.some (24 messages, latest: Feb 17 2022 at 19:20)
- mul_infi_of_nonneg (3 messages, latest: Feb 17 2022 at 18:06)
- β uncoerce equality (6 messages, latest: Feb 17 2022 at 11:51)
- Uncountable sum diverges (4 messages, latest: Feb 17 2022 at 06:41)
- N β P as a submodule of N (11 messages, latest: Feb 15 2022 at 08:01)
- Cobordism hypothesis (5 messages, latest: Feb 15 2022 at 04:42)
- Rational basis of a number field (16 messages, latest: Feb 14 2022 at 21:33)
- co-bounded filter (73 messages, latest: Feb 14 2022 at 17:28)
- Holder inequality (3 messages, latest: Feb 14 2022 at 13:39)
- (R ββ[R] M) β M (4 messages, latest: Feb 14 2022 at 12:28)
- replacement of
finset.sum_hom
(7 messages, latest: Feb 13 2022 at 20:44) - Lifting order structure (7 messages, latest: Feb 13 2022 at 12:07)
- integral sum measure (6 messages, latest: Feb 13 2022 at 01:39)
- finite categories (15 messages, latest: Feb 13 2022 at 01:13)
- Some missing prod stuff (57 messages, latest: Feb 12 2022 at 23:37)
- [generalize at ](topic/generalize.20at.20.html) (3 messages, latest: Feb 12 2022 at 21:27)
- Bijections and Inverses, Cauchy sequence permutations (6 messages, latest: Feb 12 2022 at 20:55)
- primer on set_option (12 messages, latest: Feb 12 2022 at 19:44)
- (no topic) (15 messages, latest: Feb 12 2022 at 10:02)
- Bijections and Inverses (28 messages, latest: Feb 12 2022 at 00:44)
- Functions are unequal if they disagree somewhere (16 messages, latest: Feb 11 2022 at 22:29)
- set.finite of subset range (7 messages, latest: Feb 11 2022 at 15:59)
- elements of an action which fix a set (22 messages, latest: Feb 10 2022 at 09:18)
- β enat.eq_zero_iff_le_zero (8 messages, latest: Feb 09 2022 at 17:47)
- a convex set is null measurable (6 messages, latest: Feb 09 2022 at 15:02)
- β heq_congr? (10 messages, latest: Feb 09 2022 at 06:13)
- polynomial/finsupp to list (3 messages, latest: Feb 09 2022 at 01:51)
- Partial derivatives (28 messages, latest: Feb 08 2022 at 22:47)
- mul_neg, neg_mul (4 messages, latest: Feb 08 2022 at 22:08)
- set Ξ± in fintype Ξ± (37 messages, latest: Feb 08 2022 at 22:00)
- opinionated formatter Γ la black (4 messages, latest: Feb 08 2022 at 10:13)
- heq_congr? (5 messages, latest: Feb 08 2022 at 03:10)
- Exactness in opposite category (4 messages, latest: Feb 07 2022 at 18:09)
- [le and eq iff ](topic/le.20and.20eq.20iff.20.html) (7 messages, latest: Feb 07 2022 at 09:22)
- Sub-variables (3 messages, latest: Feb 07 2022 at 08:01)
- subtype as a fintype (12 messages, latest: Feb 06 2022 at 01:17)
- β pi subgroups (22 messages, latest: Feb 05 2022 at 13:48)
- Compact opens (38 messages, latest: Feb 05 2022 at 13:34)
- β Range factorization with subtype? (13 messages, latest: Feb 05 2022 at 08:54)
- Free strict n-categories (6 messages, latest: Feb 05 2022 at 08:08)
- finset.max! (5 messages, latest: Feb 04 2022 at 23:11)
- prod version of nat.coprime.lcm_eq_mul (15 messages, latest: Feb 04 2022 at 22:15)
- β order_dual infi supr (4 messages, latest: Feb 04 2022 at 16:57)
- Wlog in the usual sense (5 messages, latest: Feb 04 2022 at 12:22)
- β Generalization of
set.image_inter_on
(1 message, latest: Feb 04 2022 at 03:12) - Generalization of
set.image_inter_on
(7 messages, latest: Feb 04 2022 at 00:26) - induction on an index type (20 messages, latest: Feb 03 2022 at 18:47)
- Counterpart of rw for modeq (4 messages, latest: Feb 03 2022 at 18:44)
- pi subgroups (16 messages, latest: Feb 03 2022 at 16:50)
- Lift composition with quot.mk (9 messages, latest: Feb 02 2022 at 21:46)
- Merge (ordered) streams (5 messages, latest: Feb 02 2022 at 17:40)
- Semigroupoidal category (16 messages, latest: Feb 02 2022 at 14:29)
- Bipointed (2 messages, latest: Feb 02 2022 at 10:15)
- transcendence of pi (13 messages, latest: Feb 02 2022 at 09:19)
- zify and divisibility (4 messages, latest: Feb 01 2022 at 21:31)
- Sum of Inf is Inf of sum (14 messages, latest: Feb 01 2022 at 16:43)
- β pi.single but for multiplicative groups (2 messages, latest: Feb 01 2022 at 16:30)
- pi.single but for multiplicative groups (2 messages, latest: Feb 01 2022 at 09:28)
- proving equality of cartesian product (5 messages, latest: Feb 01 2022 at 03:56)
- β fderiv equal to has_fderiv (4 messages, latest: Feb 01 2022 at 00:10)
- Decidable rels on a quotient (5 messages, latest: Jan 29 2022 at 22:35)
- Predicate for an element being an inverse in a comm_monoid (5 messages, latest: Jan 28 2022 at 12:20)
- β Pretty printing of equivalence classes (17 messages, latest: Jan 28 2022 at 04:08)
- Multiset min/max (2 messages, latest: Jan 27 2022 at 20:13)
- product of surjective functions is surjective (7 messages, latest: Jan 27 2022 at 20:07)
- Lindelof spaces (34 messages, latest: Jan 27 2022 at 16:10)
- Pretty printing of equivalence classes (13 messages, latest: Jan 27 2022 at 14:02)
- β injections to equiv (6 messages, latest: Jan 26 2022 at 21:18)
- integral is continuously differentiable (11 messages, latest: Jan 26 2022 at 17:40)
- pw_filter is maximal (5 messages, latest: Jan 26 2022 at 16:29)
- Quotient of a quotient (14 messages, latest: Jan 26 2022 at 14:16)
- ordered_comm_monoid_with_zero (5 messages, latest: Jan 26 2022 at 14:04)
- Least extended natural with witness (5 messages, latest: Jan 26 2022 at 09:38)
- Is this a valid way of defining a typeclass? (146 messages, latest: Jan 26 2022 at 02:09)
- Multiindex notation (14 messages, latest: Jan 25 2022 at 21:03)
- Localization of ordered integral domains (6 messages, latest: Jan 25 2022 at 10:25)
- β β>0 (33 messages, latest: Jan 25 2022 at 07:34)
- show with turnstile (7 messages, latest: Jan 24 2022 at 21:11)
- any cover admits a countable subcover (9 messages, latest: Jan 24 2022 at 18:48)
- Complete destruction tactic (35 messages, latest: Jan 24 2022 at 12:58)
- Complement is strictly antitone (5 messages, latest: Jan 23 2022 at 21:17)
- Bitopological spaces (1 message, latest: Jan 21 2022 at 21:20)
- char is some prime given prime is zero (4 messages, latest: Jan 21 2022 at 14:09)
- β
inv_mul_eq_iff_eq_mulβ
for ennreal (1 message, latest: Jan 20 2022 at 14:38) - data.nat.parity (10 messages, latest: Jan 20 2022 at 14:31)
- tactic for proving iff (1 message, latest: Jan 20 2022 at 12:45)
- β Continuous linear map to normed group hom (1 message, latest: Jan 20 2022 at 08:57)
inv_mul_eq_iff_eq_mulβ
for ennreal (5 messages, latest: Jan 20 2022 at 03:04)- weaker conditions for showing algebraically closed (3 messages, latest: Jan 19 2022 at 21:33)
- Continuous linear map to normed group hom (17 messages, latest: Jan 19 2022 at 18:29)
- bUnion for set (28 messages, latest: Jan 18 2022 at 20:57)
- Mochizuki proof of abc conjecture (3 messages, latest: Jan 16 2022 at 16:42)
- β some power of 1/2 less than a positive real (4 messages, latest: Jan 16 2022 at 09:26)
- β set singletons injective (2 messages, latest: Jan 15 2022 at 11:00)
- Thickening and closed thickening (19 messages, latest: Jan 14 2022 at 23:12)
- injections to equiv (61 messages, latest: Jan 14 2022 at 17:38)
- Union of singletons (4 messages, latest: Jan 14 2022 at 17:20)
- set singletons injective (8 messages, latest: Jan 14 2022 at 15:43)
- finsupp.map_range (2 messages, latest: Jan 14 2022 at 06:42)
- linear maps of polynomials (21 messages, latest: Jan 13 2022 at 20:22)
- fintype arrow (10 messages, latest: Jan 13 2022 at 17:01)
- nat-bezout (29 messages, latest: Jan 13 2022 at 14:52)
- pow_cancel_left (4 messages, latest: Jan 13 2022 at 10:37)
- random number generator (18 messages, latest: Jan 13 2022 at 04:27)
- dfinsupp sum ite (9 messages, latest: Jan 12 2022 at 22:37)
- Disjoint union of posets (96 messages, latest: Jan 11 2022 at 22:52)
- Epi iff surjective in
Ab
. (2 messages, latest: Jan 11 2022 at 22:41) - function on a union (3 messages, latest: Jan 11 2022 at 15:58)
- min and max of finsupps (16 messages, latest: Jan 11 2022 at 15:42)
- Generalization of mul_eq_one_comm (15 messages, latest: Jan 11 2022 at 13:52)
- mv_polynomial.total_degree of sum (7 messages, latest: Jan 11 2022 at 12:48)
- Disjoint union of finsets (10 messages, latest: Jan 11 2022 at 10:26)
- sub_group_with_zero (4 messages, latest: Jan 11 2022 at 07:37)
- Order on a quotient group (1 message, latest: Jan 10 2022 at 21:01)
- β polynomials spanned by monomials (2 messages, latest: Jan 10 2022 at 11:43)
- polynomials spanned by monomials (4 messages, latest: Jan 10 2022 at 09:05)
- mul_sup for non-negative reals (17 messages, latest: Jan 09 2022 at 18:44)
- 2^n >= n^m (48 messages, latest: Jan 07 2022 at 22:31)
- Regressive induction (15 messages, latest: Jan 07 2022 at 20:23)
- mccoy's theorem (2 messages, latest: Jan 07 2022 at 20:03)
- enumerate nonempty lists (16 messages, latest: Jan 07 2022 at 14:59)
- tactic for specificed commutativity and associativity? (3 messages, latest: Jan 07 2022 at 02:06)
- generalised eventually_at_top (14 messages, latest: Jan 06 2022 at 18:40)
- antiderivative (37 messages, latest: Jan 06 2022 at 18:11)
- Abstracting * and / (21 messages, latest: Jan 06 2022 at 14:00)
- Minimal elements and descending chains (33 messages, latest: Jan 06 2022 at 09:42)
- Criterion for
set.finite
from finsets (3 messages, latest: Jan 05 2022 at 20:13) - set.card_to_finset_univ (32 messages, latest: Jan 04 2022 at 23:43)
- real.log in other base (6 messages, latest: Jan 04 2022 at 21:46)
- opposite multiplication for subgroups (7 messages, latest: Jan 04 2022 at 16:20)
- β f^[n] x = x (13 messages, latest: Jan 03 2022 at 04:56)
- Ring for vector spaces (17 messages, latest: Jan 02 2022 at 22:33)
- Minimal relation satisfying
trans_gen
(14 messages, latest: Jan 02 2022 at 20:09) - nonemptiness tactic (5 messages, latest: Jan 02 2022 at 17:06)
- f^[n] x = x (4 messages, latest: Jan 01 2022 at 14:03)
- Prop-valued "I am a finite type" (3 messages, latest: Dec 31 2021 at 17:32)
- Multiset functor map with erase_dup (17 messages, latest: Dec 31 2021 at 16:22)
- x in subobject (O(K)) -> (x : K) in subobject K (4 messages, latest: Dec 30 2021 at 22:20)
- flip eq curry swap uncurry (2 messages, latest: Dec 30 2021 at 18:08)
- nat.nat_one_eq_one (16 messages, latest: Dec 30 2021 at 01:13)
- tensor calculus (4 messages, latest: Dec 29 2021 at 16:10)
- (lβ S).map Ο β€ lβ (S.map βΟ) (31 messages, latest: Dec 28 2021 at 23:31)
- eventually eventually (11 messages, latest: Dec 28 2021 at 22:18)
- Dual to
option.mem_unique
? (12 messages, latest: Dec 28 2021 at 22:09) - β Bounds along filters (11 messages, latest: Dec 28 2021 at 02:17)
- Additive is_scalar_tower (13 messages, latest: Dec 27 2021 at 21:08)
- Unique factorization of complex polynomials (8 messages, latest: Dec 27 2021 at 16:33)
- Continuous bijective from compact to T1 implies homeomorphis (24 messages, latest: Dec 27 2021 at 15:28)
- β ultrafilter is principal if it contains a finite set (2 messages, latest: Dec 27 2021 at 14:57)
- Ξ± β* Ξ² typeclasses (8 messages, latest: Dec 27 2021 at 11:13)
- ultrafilter is principal if it contains a finite set (13 messages, latest: Dec 27 2021 at 09:29)
- -1 ^ n (15 messages, latest: Dec 26 2021 at 03:00)
- β Measurable of constant on intervals (1 message, latest: Dec 25 2021 at 18:19)
- Measurable of constant on intervals (4 messages, latest: Dec 25 2021 at 18:11)
- U' β V β Hom(U, V) (5 messages, latest: Dec 25 2021 at 14:41)
- preorder (opposite X) (30 messages, latest: Dec 25 2021 at 01:17)
- β every type can be well-ordered (3 messages, latest: Dec 24 2021 at 02:44)
- every type can be well-ordered (1 message, latest: Dec 24 2021 at 02:27)
- Functoriality of finset (25 messages, latest: Dec 23 2021 at 22:35)
- Power series (21 messages, latest: Dec 23 2021 at 19:49)
- Long line (3 messages, latest: Dec 23 2021 at 17:11)
- Multiply
is_lub
(9 messages, latest: Dec 23 2021 at 07:20) - filtered finset cardinality (3 messages, latest: Dec 22 2021 at 22:02)
- [Writing n as p^km](topic/Writing.20n.20as.20p.5Ekm.html) (20 messages, latest: Dec 22 2021 at 18:44)
- sum nonnegative iff elements nonnegative (5 messages, latest: Dec 22 2021 at 10:12)
- Applying ring_equiv.to_ring_hom (9 messages, latest: Dec 22 2021 at 00:07)
- Lifting is_empty instance (6 messages, latest: Dec 21 2021 at 23:55)
- fin n combinatorics (18 messages, latest: Dec 21 2021 at 15:39)
- coinduced/product topologies (16 messages, latest: Dec 20 2021 at 23:16)
- Dependent forall_congr (5 messages, latest: Dec 20 2021 at 23:13)
- Compositum of finite field extensions is finite (24 messages, latest: Dec 20 2021 at 22:34)
- polynomial.eval_evalβ (12 messages, latest: Dec 20 2021 at 01:02)
- normal extension = normal subgroup (2 messages, latest: Dec 20 2021 at 00:11)
- finsupp.pi (30 messages, latest: Dec 19 2021 at 19:38)
- Computational sum_four_squares (27 messages, latest: Dec 19 2021 at 16:23)
- Normal closure of subfield exists and is finite dimensional (3 messages, latest: Dec 19 2021 at 12:51)
- strict_mono on int (4 messages, latest: Dec 19 2021 at 11:47)
- exists a unique nth element of fin n (5 messages, latest: Dec 18 2021 at 00:18)
- naming help (14 messages, latest: Dec 17 2021 at 20:47)
- Equivalences between containers induced elementwise (13 messages, latest: Dec 17 2021 at 18:03)
- card_filter_fin_lt (5 messages, latest: Dec 17 2021 at 16:01)
- not xor (6 messages, latest: Dec 17 2021 at 12:57)
- Preorder on dfinsupp (6 messages, latest: Dec 17 2021 at 12:25)
- finset.to_list sum (34 messages, latest: Dec 17 2021 at 09:54)
- β monoid_hom from additive to multiplicative structures (2 messages, latest: Dec 17 2021 at 04:14)
- monoid_hom from additive to multiplicative structures (11 messages, latest: Dec 17 2021 at 00:35)
- sqrt (r : \C) * sqrt r (5 messages, latest: Dec 16 2021 at 22:39)
- Algebras over Witt vectors (3 messages, latest: Dec 16 2021 at 21:43)
- β formal power series (2 messages, latest: Dec 16 2021 at 16:07)
- has_pow_of_has_one_has_mul (12 messages, latest: Dec 16 2021 at 15:33)
- finite domain -> finsupp (3 messages, latest: Dec 16 2021 at 13:22)
- computable_pred and primcodable β (4 messages, latest: Dec 16 2021 at 13:18)
- β Quotient of Pi type equivalent to Pi of quotient type (2 messages, latest: Dec 16 2021 at 05:02)
- Quotient of Pi type equivalent to Pi of quotient type (1 message, latest: Dec 16 2021 at 02:21)
- Concrete fraction ring of int (31 messages, latest: Dec 15 2021 at 22:24)
- formal power series (1 message, latest: Dec 15 2021 at 22:07)
- restrict linear equiv to submodules (9 messages, latest: Dec 15 2021 at 15:55)
- prod.tendsto_iff (6 messages, latest: Dec 15 2021 at 09:08)
- order_iso for ennreal rpow (16 messages, latest: Dec 14 2021 at 23:03)
- finset.subsingleton (1 message, latest: Dec 14 2021 at 18:01)
- non finsupp finsupp.dom_congr (4 messages, latest: Dec 14 2021 at 11:19)
- β linear_map.to_span_singleton as an equiv (3 messages, latest: Dec 14 2021 at 10:29)
- β Add group structure on localization (18 messages, latest: Dec 12 2021 at 17:09)
- Equivalent of
nat.find
for positive integers? (26 messages, latest: Dec 12 2021 at 12:52) - strict mono f on well-order β x β€ f x (6 messages, latest: Dec 12 2021 at 03:24)
imp_trans
(8 messages, latest: Dec 12 2021 at 00:59)- Units of product of topological rings (6 messages, latest: Dec 11 2021 at 18:19)
- equal of le and not lt (7 messages, latest: Dec 11 2021 at 13:49)
- Indexed equality (2 messages, latest: Dec 10 2021 at 18:00)
- order on | (3 messages, latest: Dec 10 2021 at 10:55)
- Big-Oh notation (5 messages, latest: Dec 10 2021 at 10:52)
- Local homeomorphisms (5 messages, latest: Dec 10 2021 at 07:37)
- β Disjoint Union of Graphs, or type overrides (12 messages, latest: Dec 09 2021 at 22:06)
- Disjoint Union of Graphs, or type overrides (1 message, latest: Dec 09 2021 at 20:53)
- polynomial.to_finsupp_iso_linear (2 messages, latest: Dec 08 2021 at 14:37)
- adjoin_eq_Inf (14 messages, latest: Dec 08 2021 at 12:20)
- list.fin_range_succ (10 messages, latest: Dec 07 2021 at 14:14)
- Pointwise set division (6 messages, latest: Dec 07 2021 at 14:10)
- Pointwise topology (12 messages, latest: Dec 07 2021 at 13:57)
- ennreal.frontier_Iic (24 messages, latest: Dec 07 2021 at 08:21)
- Addition of interiors (11 messages, latest: Dec 05 2021 at 12:47)
- β Direct product of posets (4 messages, latest: Dec 04 2021 at 04:25)
- Direct product of posets (5 messages, latest: Dec 04 2021 at 04:14)
- push_cast (14 messages, latest: Dec 02 2021 at 14:30)
- rational power (6 messages, latest: Dec 02 2021 at 12:25)
- ennreal.to_nnreal_le_to_nnreal (4 messages, latest: Nov 30 2021 at 18:32)
- Finite geometric sums (10 messages, latest: Nov 30 2021 at 17:51)
- Additive coercions (9 messages, latest: Nov 29 2021 at 22:22)
- integral translation (4 messages, latest: Nov 29 2021 at 15:39)
- lt add (5 messages, latest: Nov 29 2021 at 12:44)
- interior and ord_connected (4 messages, latest: Nov 28 2021 at 20:22)
- Interior of a set-level (5 messages, latest: Nov 28 2021 at 18:51)
- Order on Ξ± β Ξ² (16 messages, latest: Nov 27 2021 at 09:07)
- Smoothness of projection from pi (6 messages, latest: Nov 26 2021 at 21:33)
- Subgroup of topological group (3 messages, latest: Nov 26 2021 at 09:35)
- Conditionally complete lattice (32 messages, latest: Nov 26 2021 at 05:15)
- whiskering adjunctions (2 messages, latest: Nov 26 2021 at 04:52)
- order_of (-1) (17 messages, latest: Nov 25 2021 at 07:51)
- evaluation is right adjoint (3 messages, latest: Nov 24 2021 at 21:42)
- order_iso.map_supr (22 messages, latest: Nov 24 2021 at 15:44)
- Localization of localization (5 messages, latest: Nov 24 2021 at 14:51)
- tactic.trace (7 messages, latest: Nov 24 2021 at 13:09)
- Reindexing a dependent product (16 messages, latest: Nov 24 2021 at 12:01)
- β Product of submonoid in commutative monoid (2 messages, latest: Nov 24 2021 at 09:32)
- Product of submonoid in commutative monoid (8 messages, latest: Nov 24 2021 at 09:10)
- Covering relation (4 messages, latest: Nov 23 2021 at 09:24)
- Convergent implies bounded (13 messages, latest: Nov 23 2021 at 07:36)
- Is there a code for extracting square root? (5 messages, latest: Nov 22 2021 at 17:57)
- Is there code to apply ring in an equation (19 messages, latest: Nov 22 2021 at 17:44)
- characteristic two (1 message, latest: Nov 22 2021 at 16:28)
- Continuity of multilinear maps in finite dimensions (6 messages, latest: Nov 19 2021 at 16:17)
- finset.coe_product (5 messages, latest: Nov 19 2021 at 14:01)
- β Trivial fact about multiplication of nats (1 message, latest: Nov 19 2021 at 13:09)
- Trivial fact about multiplication of nats (11 messages, latest: Nov 19 2021 at 12:09)
- (deleted) (2 messages, latest: Nov 19 2021 at 11:24)
- Structure that recurses(?) (9 messages, latest: Nov 18 2021 at 20:03)
- Projection maps (26 messages, latest: Nov 17 2021 at 21:09)
- Probabilistic method (ErdΕs method) (1 message, latest: Nov 17 2021 at 09:56)
- function.injective fin (32 messages, latest: Nov 15 2021 at 18:34)
- β If
s : X.stalk x
, it comes from some \(F(V)\) (2 messages, latest: Nov 14 2021 at 01:37) - If
s : X.stalk x
, it comes from some \(F(V)\) (6 messages, latest: Nov 13 2021 at 20:58) - coe to monoid_algebra (9 messages, latest: Nov 13 2021 at 16:34)
- Map eq cons (5 messages, latest: Nov 13 2021 at 12:38)
- Trace of identity (9 messages, latest: Nov 11 2021 at 10:07)
- finset.lcm of positive integers is positive (3 messages, latest: Nov 10 2021 at 23:43)
- Terminal object of
cone F
(5 messages, latest: Nov 10 2021 at 09:45) - convex is supremum of affine (13 messages, latest: Nov 08 2021 at 13:54)
- ideal.span_image (12 messages, latest: Nov 08 2021 at 13:34)
- decl_pos and decl_olean for current file (1 message, latest: Nov 08 2021 at 11:25)
- canonical type with 2 terms in universe
u
(7 messages, latest: Nov 08 2021 at 01:56) - Prop-valued "I have one term" (21 messages, latest: Nov 07 2021 at 22:50)
- equality in sigma-types (19 messages, latest: Nov 06 2021 at 23:45)
- complex linear and conj linear parts (3 messages, latest: Nov 06 2021 at 18:40)
- sum.inl is an open map (10 messages, latest: Nov 05 2021 at 22:53)
- Product of i < j and j < i (22 messages, latest: Nov 05 2021 at 17:16)
- Cardinality of (fin).filter (19 messages, latest: Nov 05 2021 at 00:22)
- Smoothness of
equiv.prod_assoc
(26 messages, latest: Nov 04 2021 at 16:39) - polynomial.eval_prod for multiset (6 messages, latest: Nov 04 2021 at 14:56)
- The kernel of a mapped polynomial is the map of the kernel (6 messages, latest: Nov 04 2021 at 11:40)
- Use "string" instead of "parse texpr" in interactive tactics (2 messages, latest: Nov 04 2021 at 03:08)
- is_iso_ΞΉ_of_forall_is_iso (3 messages, latest: Nov 04 2021 at 02:20)
- order isomorphisms preserve disjointness (32 messages, latest: Nov 03 2021 at 21:24)
- filter nones (6 messages, latest: Nov 03 2021 at 21:06)
- homeomorphism between a normed space and a ball (3 messages, latest: Nov 03 2021 at 04:48)
- graded rings (86 messages, latest: Nov 02 2021 at 22:58)
- 4th isomorphism theorem (7 messages, latest: Nov 02 2021 at 18:22)
- Duplicated pow lemmas (3 messages, latest: Nov 02 2021 at 17:16)
- Differentiable from deriv β 0 (2 messages, latest: Nov 02 2021 at 14:42)
- quot.exact given equivalence (7 messages, latest: Nov 02 2021 at 11:22)
- fin_cases on variables (19 messages, latest: Nov 01 2021 at 18:42)
- Smoothness of linear evaluation map (5 messages, latest: Nov 01 2021 at 13:42)
- Perfect matching (2 messages, latest: Oct 30 2021 at 18:59)
- mul_inv_rev for ring_hom.inverse (19 messages, latest: Oct 29 2021 at 18:26)
- ring.inverse equals has_inv.inv (3 messages, latest: Oct 29 2021 at 13:28)
- finset to list (29 messages, latest: Oct 28 2021 at 17:14)
- intermediate_field.adjoin_splits (2 messages, latest: Oct 27 2021 at 22:05)
- Python <-> Lean (6 messages, latest: Oct 27 2021 at 20:31)
- alg_hom from intermediate_field le (8 messages, latest: Oct 27 2021 at 14:57)
- Ico_succ_left_eq_erase_Ico (7 messages, latest: Oct 27 2021 at 12:28)
- counting function (417 messages, latest: Oct 27 2021 at 07:11)
- Multiset subset decidability (1 message, latest: Oct 26 2021 at 12:27)
- Measurability of euclidean space (16 messages, latest: Oct 26 2021 at 11:47)
- modus tollens in context (6 messages, latest: Oct 26 2021 at 06:30)
- A bdd_above set of finsets is finite (18 messages, latest: Oct 25 2021 at 19:28)
- β ring homomorphism commuting with direct sum inclusion (2 messages, latest: Oct 25 2021 at 17:18)
- ring homomorphism commuting with direct sum inclusion (4 messages, latest: Oct 25 2021 at 17:15)
- Passing coe through a sum (3 messages, latest: Oct 24 2021 at 04:58)
- ite.intro (8 messages, latest: Oct 23 2021 at 22:29)
- Search engine (11 messages, latest: Oct 23 2021 at 01:48)
- list.blend (6 messages, latest: Oct 23 2021 at 01:47)
- β equal prime powers (1 message, latest: Oct 22 2021 at 21:29)
- Preconnection in sigma (26 messages, latest: Oct 22 2021 at 14:25)
- Wedderburn's little theorem (18 messages, latest: Oct 22 2021 at 12:20)
- equal prime powers (20 messages, latest: Oct 21 2021 at 19:53)
- β Should
linearith
be able to solve this? (1 message, latest: Oct 21 2021 at 10:28) - Should
linearith
be able to solve this? (6 messages, latest: Oct 21 2021 at 07:43) - Kuratowski's theorem (3 messages, latest: Oct 20 2021 at 21:42)
- Preterms/Terms, Preformulas/Formulas (9 messages, latest: Oct 20 2021 at 15:00)
- Cardinality of subgroup (38 messages, latest: Oct 20 2021 at 14:32)
- linear_map_bound_of_ball_bound (13 messages, latest: Oct 20 2021 at 14:31)
- Lattice (module) (8 messages, latest: Oct 20 2021 at 07:06)
- β dimension of direct sum (16 messages, latest: Oct 19 2021 at 14:08)
- Choose multiples outside of an ideal (3 messages, latest: Oct 18 2021 at 18:01)
- decompose conjuction/existence chain (4 messages, latest: Oct 17 2021 at 15:01)
- inversion (10 messages, latest: Oct 17 2021 at 01:54)
- Dirichlet's theorem on arithmetic progressions? (23 messages, latest: Oct 16 2021 at 23:45)
- Integral of complex functions (5 messages, latest: Oct 16 2021 at 20:22)
- Affine independent finset (2 messages, latest: Oct 16 2021 at 20:10)
- uniform convergence on a compact set (3 messages, latest: Oct 15 2021 at 19:08)
- Simple algebra / ring (46 messages, latest: Oct 15 2021 at 17:45)
- finset.sup_attach (7 messages, latest: Oct 15 2021 at 08:36)
- Linear basis from spanning set (15 messages, latest: Oct 14 2021 at 19:47)
- Inf and Sup of smul of a set (39 messages, latest: Oct 14 2021 at 08:33)
- set_like disjoint (2 messages, latest: Oct 13 2021 at 19:08)
- The nonnegative elements (17 messages, latest: Oct 13 2021 at 14:06)
- β Cardinality of subtype as a sum (7 messages, latest: Oct 13 2021 at 12:17)
- Cardinality of subtype as a sum (3 messages, latest: Oct 13 2021 at 00:28)
- Things for which there was no documentation i could find (97 messages, latest: Oct 12 2021 at 20:54)
- Cantor_Bernstein (16 messages, latest: Oct 12 2021 at 16:17)
- fintype_of_fintype_ne (29 messages, latest: Oct 12 2021 at 14:18)
- strict_mono_subseq (4 messages, latest: Oct 12 2021 at 13:25)
- [Definitional lemmas for βͺ, β«β](topic/Definitional.20lemmas.20for.20.E2.9F.AA.2C.20.E2.9F.AB.E2.84.82.html) (12 messages, latest: Oct 11 2021 at 20:43)
- Direct sum on fintype (5 messages, latest: Oct 11 2021 at 17:43)
- β mapping a fintype into a finset (4 messages, latest: Oct 11 2021 at 08:07)
- finset.drop_none (13 messages, latest: Oct 10 2021 at 16:23)
- β group to group_with_zero (2 messages, latest: Oct 09 2021 at 22:13)
- group to group_with_zero (2 messages, latest: Oct 09 2021 at 22:10)
- modus ponens in context (23 messages, latest: Oct 09 2021 at 17:46)
- le_mul_of_one_le_of_le' for reals (6 messages, latest: Oct 08 2021 at 21:10)
- finset.extend_by_zero variant (25 messages, latest: Oct 08 2021 at 14:50)
- Provability logics (1 message, latest: Oct 08 2021 at 13:32)
- β nat.log is monotonically decreasing on its first argument (3 messages, latest: Oct 08 2021 at 10:15)
- category of objects with distinguished endomorphism (7 messages, latest: Oct 06 2021 at 21:16)
- two_le_add_inv (8 messages, latest: Oct 05 2021 at 15:56)
- smul_pos (3 messages, latest: Oct 05 2021 at 08:10)
- Infinite series is summable iff 'tail' of series is summable (4 messages, latest: Oct 04 2021 at 21:00)
- β Matrix automation??? (6 messages, latest: Oct 04 2021 at 16:28)
- Matrix automation??? (5 messages, latest: Oct 04 2021 at 16:11)
- Convergence of a complex series bounded by a geometric sum (7 messages, latest: Oct 04 2021 at 12:37)
- nat.log is monotonically decreasing on its first argument (21 messages, latest: Oct 04 2021 at 10:23)
- not_def (4 messages, latest: Oct 03 2021 at 20:55)
- nonempty_of_nonempty_subtype (3 messages, latest: Oct 03 2021 at 15:47)
- order_iso.map_cInf (3 messages, latest: Oct 03 2021 at 08:30)
- (lean 4) witness from (decide p && .. && decide n) (18 messages, latest: Sep 30 2021 at 21:35)
- β supr over units β€ (2 messages, latest: Sep 30 2021 at 14:32)
- Expression printed as AST (5 messages, latest: Sep 30 2021 at 14:05)
- supr over units β€ (8 messages, latest: Sep 30 2021 at 12:47)
- extract sublist from list (6 messages, latest: Sep 29 2021 at 08:52)
- no injective function on
ordinal
(2 messages, latest: Sep 28 2021 at 13:26) - equiv.symm_trans_rev (3 messages, latest: Sep 28 2021 at 10:49)
- sum.elim on function operations (4 messages, latest: Sep 28 2021 at 07:18)
- value multiplied by a unit is associated (6 messages, latest: Sep 27 2021 at 12:28)
- pi_eq_sum_univ for finsupp (28 messages, latest: Sep 25 2021 at 20:50)
- Grid adjacency graph (9 messages, latest: Sep 24 2021 at 19:00)
- ite_eq_imp_iff (6 messages, latest: Sep 24 2021 at 18:33)
- Restricting domains of functions (9 messages, latest: Sep 24 2021 at 18:06)
- inf_Sup_right (28 messages, latest: Sep 24 2021 at 15:04)
- normed space real of complex (11 messages, latest: Sep 24 2021 at 13:41)
- is_zero_object (4 messages, latest: Sep 23 2021 at 17:51)
- mapping a fintype into a finset (12 messages, latest: Sep 23 2021 at 12:20)
- prime_or_zero for naturals (10 messages, latest: Sep 21 2021 at 18:59)
- cases matching with (10 messages, latest: Sep 21 2021 at 09:45)
- Continuity on basic opens (9 messages, latest: Sep 20 2021 at 23:33)
- Decimal expansion (3 messages, latest: Sep 20 2021 at 18:19)
- succ-free induction on nat (3 messages, latest: Sep 20 2021 at 17:44)
- β Rings of char p are a
zmod p
algebra (5 messages, latest: Sep 19 2021 at 11:47) - Field of Fractions (4 messages, latest: Sep 18 2021 at 18:24)
- Diagonalization of symmetric matrices (3 messages, latest: Sep 18 2021 at 17:10)
- finset.center_mass as a linear map (4 messages, latest: Sep 17 2021 at 17:47)
- β Change of basis (4 messages, latest: Sep 17 2021 at 11:37)
- x^p is concave for 0 <= p <= 1 (13 messages, latest: Sep 17 2021 at 10:47)
- Gluing of [continuous] functions (21 messages, latest: Sep 17 2021 at 05:13)
- add_lt_of_lt_sub (9 messages, latest: Sep 16 2021 at 22:00)
- maximum of a function (5 messages, latest: Sep 16 2021 at 20:38)
- Selecting element from finite type (21 messages, latest: Sep 16 2021 at 16:21)
- eval2 for alg_homs (3 messages, latest: Sep 14 2021 at 19:16)
- specializing forall to a set (6 messages, latest: Sep 14 2021 at 10:44)
- Polynomial from coefficients (10 messages, latest: Sep 11 2021 at 15:11)
- β differentiation on
mv_polynomial
(5 messages, latest: Sep 11 2021 at 13:29) - total_on (3 messages, latest: Sep 11 2021 at 10:54)
- Standard inclusion R^n β R^{n+1} (32 messages, latest: Sep 10 2021 at 15:36)
- Generate explanation for expressions (11 messages, latest: Sep 10 2021 at 09:12)
- β Burnside's Lemma & Polya theorem (1 message, latest: Sep 10 2021 at 07:53)
- β Perron-Frobenius Theorem, Cauchy's Interlacing Theorem? (1 message, latest: Sep 10 2021 at 07:53)
- differentiation on
mv_polynomial
(6 messages, latest: Sep 10 2021 at 05:01) - Perron-Frobenius Theorem, Cauchy's Interlacing Theorem? (6 messages, latest: Sep 10 2021 at 04:56)
- Burnside's Lemma & Polya theorem (8 messages, latest: Sep 10 2021 at 04:23)
- Units and Jacobson radical (2 messages, latest: Sep 09 2021 at 22:10)
- β Universal Property of finsupp (5 messages, latest: Sep 09 2021 at 15:50)
- β Basis of matrices (1 message, latest: Sep 09 2021 at 14:43)
- trivial group quotient (12 messages, latest: Sep 09 2021 at 10:52)
- Maximal elements of a partial order (8 messages, latest: Sep 08 2021 at 18:55)
- β integral Union (2 messages, latest: Sep 08 2021 at 17:20)
- subsingleton (set A) of is_empty A (12 messages, latest: Sep 08 2021 at 13:43)
- inequality of prod constructor (12 messages, latest: Sep 08 2021 at 13:15)
- nonzero thing in
with_zero X
(7 messages, latest: Sep 07 2021 at 20:48) - Basis of matrices (4 messages, latest: Sep 07 2021 at 15:40)
- integral Union (1 message, latest: Sep 07 2021 at 14:52)
- Chicken Mcnugget/Frobenius coin (13 messages, latest: Sep 06 2021 at 23:45)
- β Vector heq (4 messages, latest: Sep 06 2021 at 22:32)
- viewing an expanded term (10 messages, latest: Sep 06 2021 at 20:44)
- map out of algebra.adjoin (9 messages, latest: Sep 06 2021 at 16:36)
- imp_iff_imp_left (2 messages, latest: Sep 06 2021 at 14:14)
- funext for inequalities (45 messages, latest: Sep 06 2021 at 07:36)
- complete_linear_ordered_add_comm_monoid (9 messages, latest: Sep 06 2021 at 06:46)
- Defining function on union (15 messages, latest: Sep 05 2021 at 21:22)
- Vector heq (1 message, latest: Sep 05 2021 at 21:10)
- has_fderiv.mul in normed algebras ? (4 messages, latest: Sep 05 2021 at 21:00)
- polynomial/finsupp.update (3 messages, latest: Sep 05 2021 at 19:33)
- Directed union of subobject (3 messages, latest: Sep 05 2021 at 14:30)
- pi boolean algebra (6 messages, latest: Sep 05 2021 at 11:29)
- AM-GM (6 messages, latest: Sep 04 2021 at 14:51)
- Vandermonde's identity (9 messages, latest: Sep 04 2021 at 06:38)
- mem_iff for subsingletons (2 messages, latest: Sep 03 2021 at 23:26)
- pointwise min and max (13 messages, latest: Sep 02 2021 at 17:14)
- Sandwich product of vectors and matrices (3 messages, latest: Sep 02 2021 at 10:31)
- linear map from bilinear (8 messages, latest: Sep 02 2021 at 09:32)
- Dependent left_inverse (4 messages, latest: Sep 01 2021 at 11:22)
- Create a blueprint (25 messages, latest: Sep 01 2021 at 10:27)
- index of subgroup (8 messages, latest: Sep 01 2021 at 06:42)
- group acting on algebra (23 messages, latest: Aug 31 2021 at 19:40)
- ordered_module β β (2 messages, latest: Aug 30 2021 at 23:31)
- submodule.supr_mul (17 messages, latest: Aug 30 2021 at 22:27)
- Enumerating a finite subset (28 messages, latest: Aug 30 2021 at 13:10)
- Choosing a finset of minimum cardinality (22 messages, latest: Aug 28 2021 at 07:50)
- monoid_hom for units (13 messages, latest: Aug 27 2021 at 06:17)
- β tactic for structural equality (4 messages, latest: Aug 26 2021 at 09:52)
prod_dite_of_true
(38 messages, latest: Aug 25 2021 at 18:54)- dependent functions out of a sum equivalent to β¦ (4 messages, latest: Aug 25 2021 at 03:44)
- Hartog's theorem (9 messages, latest: Aug 23 2021 at 23:07)
- coprod and prod on submodules (15 messages, latest: Aug 23 2021 at 19:45)
- Behaviour of finrank under morphisms (32 messages, latest: Aug 22 2021 at 22:36)
- Equivalence class of a setoid (5 messages, latest: Aug 22 2021 at 22:17)
real.cos
is positive iff it is within a union of intervals (2 messages, latest: Aug 21 2021 at 19:18)- constant if fderiv is zero on connected open sets (1 message, latest: Aug 21 2021 at 06:54)
- β Eventually vacuously true statements (1 message, latest: Aug 19 2021 at 21:32)
- β derivative of (f xβ»ΒΉ) (1 message, latest: Aug 19 2021 at 21:32)
- β Asymptotics conversions from equivalents (1 message, latest: Aug 19 2021 at 21:32)
- Totally ordered subsets of a partial order (7 messages, latest: Aug 19 2021 at 20:54)
- β Conjugate of a subgroup (7 messages, latest: Aug 19 2021 at 17:21)
- Asymptotics conversions from equivalents (31 messages, latest: Aug 18 2021 at 23:49)
- Eventually vacuously true statements (4 messages, latest: Aug 18 2021 at 17:11)
- finprod of constant func (9 messages, latest: Aug 18 2021 at 14:53)
- derivative of (f xβ»ΒΉ) (4 messages, latest: Aug 18 2021 at 12:59)
- nat.smul_one_eq_coe for enat (3 messages, latest: Aug 18 2021 at 12:45)
- Proving cancellation of deriv at non-differentiable points (1 message, latest: Aug 18 2021 at 12:06)
- Divisibility to adic valuation (8 messages, latest: Aug 18 2021 at 11:19)
- Prime dividing a product (3 messages, latest: Aug 18 2021 at 08:16)
- Sigma assoc (3 messages, latest: Aug 18 2021 at 00:37)
- Moving to the limit in equalities (20 messages, latest: Aug 17 2021 at 18:14)
- Euclidean space (3 messages, latest: Aug 16 2021 at 17:24)
- complex vs real limit (28 messages, latest: Aug 15 2021 at 20:34)
- Restricting permutations (17 messages, latest: Aug 15 2021 at 19:20)
- cardinal.lift_sup (11 messages, latest: Aug 15 2021 at 02:01)
- by_contra! (10 messages, latest: Aug 13 2021 at 13:38)
- Nsatz-like tactic (3 messages, latest: Aug 13 2021 at 05:26)
- quot.forall (5 messages, latest: Aug 12 2021 at 23:34)
- real.summable_of_sum_le (6 messages, latest: Aug 11 2021 at 23:43)
- add_rpow_le (3 messages, latest: Aug 11 2021 at 06:26)
- Composition with injective function is an injective operatio (5 messages, latest: Aug 10 2021 at 15:26)
- discrete topology type alias (11 messages, latest: Aug 10 2021 at 13:04)
- Number between integers not an integer (7 messages, latest: Aug 10 2021 at 07:56)
- completion of a ring at an ideal (4 messages, latest: Aug 09 2021 at 20:18)
- Z is discrete (6 messages, latest: Aug 07 2021 at 18:49)
- differential equations (20 messages, latest: Aug 07 2021 at 17:27)
- quotient homeomorphisms (9 messages, latest: Aug 06 2021 at 19:28)
- Weierstrass M-test (12 messages, latest: Aug 06 2021 at 16:16)
- graph, expander graph, cayley graph, β¦ (10 messages, latest: Aug 06 2021 at 14:25)
- One point compactification (26 messages, latest: Aug 05 2021 at 14:44)
- injective scalar actions (14 messages, latest: Aug 05 2021 at 13:16)
- ite or (3 messages, latest: Aug 05 2021 at 13:06)
- equiv for polynomial ring over opposite ring (19 messages, latest: Aug 03 2021 at 20:03)
- cone equiv (7 messages, latest: Aug 03 2021 at 17:28)
- Example in lean (6 messages, latest: Aug 03 2021 at 01:04)
- Continuous empty map (7 messages, latest: Aug 02 2021 at 20:09)
- A submonoid of a
cancel_monoid_with_zero
also cancels (4 messages, latest: Aug 02 2021 at 15:34) - Lifting exponent lemma (6 messages, latest: Aug 02 2021 at 14:57)
- Highest prime power dividing a nat? (4 messages, latest: Aug 02 2021 at 09:22)
- Equitable functions (1 message, latest: Aug 01 2021 at 13:38)
- β Clear true tactic (2 messages, latest: Aug 01 2021 at 05:32)
- The submonoid of positive elements (5 messages, latest: Jul 31 2021 at 17:38)
- aargh dfinsupp is constructive (27 messages, latest: Jul 31 2021 at 16:45)
- Hensel's lemma (5 messages, latest: Jul 31 2021 at 13:16)
- saturating addition on the bottom (19 messages, latest: Jul 31 2021 at 10:29)
- factors lemma (30 messages, latest: Jul 30 2021 at 18:36)
- monoid_hom.map_div (4 messages, latest: Jul 29 2021 at 20:30)
- limits as a class? (18 messages, latest: Jul 29 2021 at 16:32)
- monotonicity for sums and products of monotone functions (16 messages, latest: Jul 29 2021 at 15:11)
- Combining functors (4 messages, latest: Jul 28 2021 at 20:27)
- circulant matrix (40 messages, latest: Jul 28 2021 at 17:26)
- Quotient of a ring by a sum of ideals (30 messages, latest: Jul 28 2021 at 09:36)
- multiset.sum (4 messages, latest: Jul 26 2021 at 21:58)
- β Algebra map is injective (7 messages, latest: Jul 25 2021 at 22:42)
- Algebra map is injective (7 messages, latest: Jul 25 2021 at 21:00)
- Sylow subgroups (8 messages, latest: Jul 24 2021 at 16:26)
- bilinear (3 messages, latest: Jul 23 2021 at 12:02)
- finsetoid (13 messages, latest: Jul 23 2021 at 02:39)
- open private (3 messages, latest: Jul 22 2021 at 08:30)
- getting a linear map from a span (13 messages, latest: Jul 22 2021 at 00:11)
- Local expansions of holomorphic functions (35 messages, latest: Jul 21 2021 at 23:38)
- quotient of a group by a subgroup bijects with left cosets (6 messages, latest: Jul 21 2021 at 09:41)
- If
f x β€ f y β x β€ y
, thenf
is injective (3 messages, latest: Jul 20 2021 at 13:27) - β monotone limits (1 message, latest: Jul 18 2021 at 14:19)
- β equalities with set differences (1 message, latest: Jul 18 2021 at 14:18)
- β tendsto_induced (1 message, latest: Jul 18 2021 at 14:18)
- Complex Integral of 1/z round the unit circle (30 messages, latest: Jul 17 2021 at 11:04)
- not some implies none (6 messages, latest: Jul 17 2021 at 01:20)
- tendsto_induced (4 messages, latest: Jul 16 2021 at 23:36)
- equalities with set differences (5 messages, latest: Jul 16 2021 at 15:24)
- Lifting lattice structures (2 messages, latest: Jul 16 2021 at 12:25)
- Subsequence of cauchy seq (10 messages, latest: Jul 15 2021 at 23:13)
- Finitely generated algebras, etc (29 messages, latest: Jul 15 2021 at 17:32)
- Different casts from zmod (17 messages, latest: Jul 15 2021 at 09:06)
- Construct finset from set (6 messages, latest: Jul 14 2021 at 16:45)
- Clear true tactic (9 messages, latest: Jul 14 2021 at 11:32)
- submonoid.mem_supr (4 messages, latest: Jul 13 2021 at 19:10)
- lemmas regarding Ξ΅ > 0 (7 messages, latest: Jul 13 2021 at 15:17)
- polynomial
eval_ring_hom
andeval_linear_map
(6 messages, latest: Jul 12 2021 at 18:12) - set.finite_mem_finset (3 messages, latest: Jul 12 2021 at 17:18)
- matrix det (15 messages, latest: Jul 11 2021 at 20:05)
- e as limit of (1+1/n)^n (11 messages, latest: Jul 09 2021 at 18:13)
- bex_and (11 messages, latest: Jul 08 2021 at 23:17)
- n < nat.succ m β n β€ m (7 messages, latest: Jul 08 2021 at 09:11)
- exists_mem_of_ne_empty (5 messages, latest: Jul 07 2021 at 07:03)
- maps_to.restrict_codom (21 messages, latest: Jul 06 2021 at 22:03)
- psd matrices (5 messages, latest: Jul 06 2021 at 04:09)
- Third isomorphism theorem (7 messages, latest: Jul 05 2021 at 14:30)
- compass and straightedge constructions (2 messages, latest: Jul 04 2021 at 19:05)
- Set from finset is finite (5 messages, latest: Jul 04 2021 at 13:30)
- the obvious monadic adjoint (5 messages, latest: Jul 01 2021 at 01:48)
- Congruent triangles (15 messages, latest: Jun 30 2021 at 22:55)
- abs with constant (11 messages, latest: Jun 30 2021 at 17:28)
- The unique
β ββ\[β\] A
given a square root of -1 (28 messages, latest: Jun 29 2021 at 15:49) - Collecting terms (6 messages, latest: Jun 29 2021 at 13:54)
- a + b - c = a - c + b (3 messages, latest: Jun 29 2021 at 08:47)
- The canonical
β ββ\[β\] A
given a square root of -1 (1 message, latest: Jun 28 2021 at 12:16) - The linear map to build a pure imaginary number (9 messages, latest: Jun 27 2021 at 21:54)
- connected_space.is_connected_univ (5 messages, latest: Jun 27 2021 at 18:51)
- Existence of Euler Line (5 messages, latest: Jun 25 2021 at 13:35)
- Can I render my Lean as HTML? (9 messages, latest: Jun 25 2021 at 09:19)
- Sum of functions with disjoint supports (2 messages, latest: Jun 24 2021 at 19:58)
- A β (set.univ A) (7 messages, latest: Jun 24 2021 at 13:10)
- intersection of a set and a finset as a finset (7 messages, latest: Jun 23 2021 at 15:42)
- action on a constant is a linear_map (5 messages, latest: Jun 23 2021 at 08:53)
- Homomorphism induced by left composition (11 messages, latest: Jun 23 2021 at 08:48)
- multiset ext nodup (3 messages, latest: Jun 22 2021 at 19:15)
- nat.factorial lemmas (40 messages, latest: Jun 22 2021 at 08:15)
- Factorization algebras (17 messages, latest: Jun 21 2021 at 08:54)
- R[X] is an R-algebra (6 messages, latest: Jun 19 2021 at 13:20)
- Cardinality of union of finsets (4 messages, latest: Jun 18 2021 at 17:22)
- monotone limits (28 messages, latest: Jun 18 2021 at 09:42)
- Homomorphism from the integers descends to \(\mathbb{Z}/n\) (27 messages, latest: Jun 17 2021 at 16:31)
(ideal.span {d}).quotient
iszmod d
(5 messages, latest: Jun 17 2021 at 13:36)β gmultiples
iff divides (6 messages, latest: Jun 17 2021 at 13:09)- discrete valuation (34 messages, latest: Jun 17 2021 at 13:03)
- arbitrary linear order (4 messages, latest: Jun 16 2021 at 14:15)
- V(I) /\ V(J) = V(I+J) (14 messages, latest: Jun 16 2021 at 02:53)
- Real subX associated to a complex subX (26 messages, latest: Jun 15 2021 at 14:34)
- convex_on of linear_map (3 messages, latest: Jun 14 2021 at 21:17)
- is_closed_prod (4 messages, latest: Jun 12 2021 at 13:15)
- to_module and map_range (9 messages, latest: Jun 12 2021 at 09:51)
- abelian group decomposition (11 messages, latest: Jun 11 2021 at 09:27)
- Localization of categories (12 messages, latest: Jun 10 2021 at 19:12)
- Replace metavariables by appropriate quantifiers (5 messages, latest: Jun 10 2021 at 09:46)
- type class in "forall/exists" (27 messages, latest: Jun 10 2021 at 08:46)
- Status of Cauchy's integral formula (2 messages, latest: Jun 09 2021 at 18:11)
- trivial module, etc (4 messages, latest: Jun 09 2021 at 14:26)
submodule.quotient.mk
as a linear map (7 messages, latest: Jun 08 2021 at 12:21)- linear_independent lemmas (7 messages, latest: Jun 08 2021 at 05:59)
- div_le_div (1 message, latest: Jun 07 2021 at 18:03)
- Converse of linear_equiv.congr_arg (9 messages, latest: Jun 07 2021 at 15:09)
- Getting the first element of a nonempty list (6 messages, latest: Jun 07 2021 at 13:02)
- fintype across equiv (12 messages, latest: Jun 06 2021 at 16:52)
- nat_floor (74 messages, latest: Jun 06 2021 at 08:46)
- rpow log exp inequalities (21 messages, latest: Jun 04 2021 at 14:12)
- submodule.le_span (23 messages, latest: Jun 04 2021 at 13:26)
- :golf: (9 messages, latest: Jun 04 2021 at 11:02)
- infi_insert' (1 message, latest: Jun 04 2021 at 10:58)
- homotopy groups of spheres (25 messages, latest: Jun 03 2021 at 19:19)
- Derive is_antisymm (2 messages, latest: Jun 03 2021 at 14:50)
- infinite pigeonhole (4 messages, latest: Jun 03 2021 at 05:35)
- Scalar tower of algebras (4 messages, latest: Jun 02 2021 at 20:30)
- sigma_finsupp_to_dfinsupp (12 messages, latest: Jun 02 2021 at 16:15)
- real sequences: filter.tends_to vs. classical def. (5 messages, latest: Jun 02 2021 at 10:23)
- Multiple cases at once (5 messages, latest: Jun 02 2021 at 09:57)
- topological basis on Inf topology (18 messages, latest: May 31 2021 at 22:10)
- maximal linear independent set? (11 messages, latest: May 31 2021 at 11:40)
- Transferring Instances along Equivs (22 messages, latest: May 31 2021 at 05:04)
- Induced map on homs (4 messages, latest: May 30 2021 at 10:39)
- gsmul API (7 messages, latest: May 30 2021 at 07:12)
- The simplex category (11 messages, latest: May 29 2021 at 22:17)
- Do we have CW complexes? (50 messages, latest: May 29 2021 at 19:55)
- pass between π and ring_hom.id (4 messages, latest: May 29 2021 at 12:54)
- not independent of mem span (2 messages, latest: May 29 2021 at 07:07)
fintype Ξ± β Ξ² β fintype Ξ±
(16 messages, latest: May 28 2021 at 12:56)- Image of function as finset (9 messages, latest: May 27 2021 at 19:25)
- Kernel of product morphism (18 messages, latest: May 27 2021 at 13:09)
- nnreal.le_div_iff (9 messages, latest: May 26 2021 at 17:58)
- is_compact.nonempty_inter_of⦠(5 messages, latest: May 26 2021 at 14:55)
units Rα΅α΅
and(units R)α΅α΅
are equivalent (2 messages, latest: May 26 2021 at 14:40)has_pow
(9 messages, latest: May 26 2021 at 14:35)- Riemann zeta function (8 messages, latest: May 26 2021 at 10:59)
- continuity of
coe_fn : C(Ξ±, Ξ²) β (Ξ± β Ξ²)
(4 messages, latest: May 26 2021 at 10:30) - functor.eval (7 messages, latest: May 26 2021 at 10:04)
- topology eq of homeomorph (3 messages, latest: May 25 2021 at 12:23)
- Jacobi determinant of f? (2 messages, latest: May 22 2021 at 17:22)
- what sort of lattice is needed? (9 messages, latest: May 22 2021 at 07:23)
- extension of scalars for a module, complexification (10 messages, latest: May 21 2021 at 16:02)
- direct sums of submodules (16 messages, latest: May 21 2021 at 09:31)
- submodule of a submodule (4 messages, latest: May 21 2021 at 08:15)
- Sup in nat belongs to set (22 messages, latest: May 21 2021 at 05:43)
- Disjoint union of totally disconnected spaces (7 messages, latest: May 20 2021 at 16:56)
- surjective endomorphism of a noetherian module is injective? (11 messages, latest: May 20 2021 at 02:42)
- CantorβZassenhaus or Berlekamp's algorithm (1 message, latest: May 18 2021 at 17:59)
- Complex analysis - order of vanishing (1 message, latest: May 18 2021 at 14:16)
- Propositions on rational integers (3 messages, latest: May 17 2021 at 20:28)
- Subtypes of functions are equivalent to functions to subtype (2 messages, latest: May 17 2021 at 14:00)
- Countability of eventually identity sequences (2 messages, latest: May 17 2021 at 07:32)
- switching between % and | (6 messages, latest: May 17 2021 at 07:17)
- primes in nat and int (7 messages, latest: May 15 2021 at 12:00)
- list.iterate (4 messages, latest: May 13 2021 at 22:10)
- n-ary zip_with (10 messages, latest: May 13 2021 at 19:58)
- unique from empty (42 messages, latest: May 13 2021 at 05:45)
exact
without definitional unfolding (5 messages, latest: May 11 2021 at 18:54)- Rank of a vector space (18 messages, latest: May 11 2021 at 09:03)
- monotone coercion (65 messages, latest: May 10 2021 at 16:33)
- image of finset in set (4 messages, latest: May 09 2021 at 23:31)
- split_if1 (2 messages, latest: May 09 2021 at 07:53)
- Exists unique in list (7 messages, latest: May 09 2021 at 04:30)
- Localization at units (46 messages, latest: May 08 2021 at 17:23)
- Switch current goal based on pattern (5 messages, latest: May 07 2021 at 13:59)
- pairwise implying R a b (3 messages, latest: May 07 2021 at 00:51)
- integers are closed in reals (18 messages, latest: May 06 2021 at 22:59)
- modules over a ring (35 messages, latest: May 06 2021 at 09:05)
- Splitting product-like hypotheses (3 messages, latest: May 06 2021 at 01:33)
- Absurd patterns (5 messages, latest: May 05 2021 at 17:30)
- Scalar multiplication by reals is continuous (4 messages, latest: May 05 2021 at 16:45)
- has_coe or id (3 messages, latest: May 05 2021 at 09:30)
- set to finset equiv (15 messages, latest: May 05 2021 at 06:28)
- 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
ofprod
isprod
ofperm
(8 messages, latest: May 03 2021 at 14:33)- finsum over product of types (88 messages, latest: May 02 2021 at 13:26)
- β_p and β_p (3 messages, latest: May 02 2021 at 09:21)
- continuous.sum (9 messages, latest: Apr 30 2021 at 21:28)
- fintype of surjective (5 messages, latest: Apr 30 2021 at 16:35)
- Lattice Homomorphisms? (20 messages, latest: Apr 30 2021 at 14:50)
- equivalence class (1 message, latest: Apr 30 2021 at 14:00)
- left_cancel_semigroup β (11 messages, latest: Apr 30 2021 at 08:06)
- multiplicative.of_add commutes with summation (1 message, latest: Apr 29 2021 at 16:23)
- int.div_eq_zero (5 messages, latest: Apr 28 2021 at 12:53)
- composition of locally constant maps (4 messages, latest: Apr 28 2021 at 04:54)
- ring tactics for characteristic p? (79 messages, latest: Apr 27 2021 at 18:28)
- finset.sum over fin (n+1) (4 messages, latest: Apr 26 2021 at 01:02)
- Birthday Problem (50 messages, latest: Apr 25 2021 at 15:04)
- simplify dite (5 messages, latest: Apr 25 2021 at 03:09)
- Product in
over X
vs fibered product (12 messages, latest: Apr 24 2021 at 14:44) - findim_eq_one_iff (5 messages, latest: Apr 24 2021 at 12:50)
- dfinsupp.to_finsupp (7 messages, latest: Apr 24 2021 at 08:10)
- R^m is finite dimensional over R (45 messages, latest: Apr 23 2021 at 17:31)
- has_inv.inv as a monoid_hom on groups (7 messages, latest: Apr 22 2021 at 17:51)
- searching by type (5 messages, latest: Apr 22 2021 at 09:30)
- cardinality of disjoint union (8 messages, latest: Apr 21 2021 at 17:09)
- finsupp equiv dfinsupp (2 messages, latest: Apr 20 2021 at 23:20)
- convex hull of an insert (3 messages, latest: Apr 20 2021 at 13:38)
- left/right unification (11 messages, latest: Apr 20 2021 at 12:53)
- modular forms and Hecke operators (7 messages, latest: Apr 19 2021 at 09:07)
- dist on
real
(3 messages, latest: Apr 18 2021 at 12:13) - smul_const for filters (9 messages, latest: Apr 17 2021 at 23:25)
- rational functions (17 messages, latest: Apr 17 2021 at 20:28)
- convex hulls and compact convex sets (30 messages, latest: Apr 17 2021 at 19:34)
- Minkowski Lattice Theorem (7 messages, latest: Apr 17 2021 at 06:35)
- diagram chase thingy (7 messages, latest: Apr 16 2021 at 22:10)
- continuous_on.dif (13 messages, latest: Apr 15 2021 at 21:18)
- Scaling of open set is open (11 messages, latest: Apr 15 2021 at 17:42)
- Linear map is continuous if it's continuous at zero (9 messages, latest: Apr 15 2021 at 16:59)
- positive reals (18 messages, latest: Apr 15 2021 at 07:47)
- Additive/Multiplicative closure (10 messages, latest: Apr 15 2021 at 07:40)
- max over compact of continuous (7 messages, latest: Apr 15 2021 at 07:35)
- direct_sum.to_add_monoid_apply (14 messages, latest: Apr 14 2021 at 21:39)
- by symmetry (28 messages, latest: Apr 14 2021 at 08:40)
- Inf of scalar product (3 messages, latest: Apr 13 2021 at 22:50)
- finset.sup' (51 messages, latest: Apr 13 2021 at 07:44)
- Barycentric coordinates (7 messages, latest: Apr 12 2021 at 22:23)
- For naturals m < m', there is a positive integer s.thβ¦. (12 messages, latest: Apr 12 2021 at 20:08)
- Graphs and paths in graphs (40 messages, latest: Apr 11 2021 at 03:05)
- Functorial version of obj (5 messages, latest: Apr 10 2021 at 23:36)
- order dot final (2 messages, latest: Apr 10 2021 at 16:39)
- mul_right_comm_monoid (2 messages, latest: Apr 10 2021 at 00:05)
- total preorder to linear order (18 messages, latest: Apr 09 2021 at 20:50)
- set membership (4 messages, latest: Apr 09 2021 at 20:20)
fintype.equiv_fin
+fin.cast
(29 messages, latest: Apr 09 2021 at 16:19)- tangent bundle is a topological_vector_bundle (10 messages, latest: Apr 09 2021 at 09:00)
- iterate.comm (73 messages, latest: Apr 09 2021 at 07:02)
- exists simplifying ors (3 messages, latest: Apr 08 2021 at 07:31)
- negation of funext? (8 messages, latest: Apr 07 2021 at 14:03)
- Powers of a relation? (8 messages, latest: Apr 07 2021 at 01:57)
- Root Exports (15 messages, latest: Apr 06 2021 at 20:59)
- Ascending chain conditions (38 messages, latest: Apr 06 2021 at 20:07)
- is_closed.graph (12 messages, latest: Apr 06 2021 at 15:02)
- Symmetric matrix eigen-decomposition (7 messages, latest: Apr 06 2021 at 11:58)
- Homeomorphisms between [0,1] and [a,b]? (4 messages, latest: Apr 06 2021 at 08:09)
- equiv.set renamed? (3 messages, latest: Apr 06 2021 at 07:07)
- finset.subset_iff_inter_eq_left / right (14 messages, latest: Apr 06 2021 at 05:31)
- fintype.of_finset alternative (4 messages, latest: Apr 05 2021 at 23:24)
- Eventually monotone sequences converge (7 messages, latest: Apr 05 2021 at 22:42)
- set.finite.of_surjective (3 messages, latest: Apr 05 2021 at 22:01)
- continuous.of_locally_constant (9 messages, latest: Apr 05 2021 at 20:07)
- divisor dividend and remained for nat (3 messages, latest: Apr 05 2021 at 16:59)
- product tends to zero (22 messages, latest: Apr 05 2021 at 16:51)
- {0 -> 1} as a category (10 messages, latest: Apr 02 2021 at 18:51)
- Sums over finsets and fintypes (9 messages, latest: Apr 02 2021 at 12:22)
algebra_map.injective.linear_independent
(5 messages, latest: Apr 01 2021 at 18:57)- transitive group action (14 messages, latest: Apr 01 2021 at 14:32)
- inequality lemma (18 messages, latest: Mar 31 2021 at 23:38)
- pullbacks in Type u (9 messages, latest: Mar 31 2021 at 07:42)
- Urysohn's Lemma? (6 messages, latest: Mar 30 2021 at 21:18)
- has_terminal.of_is_terminal (5 messages, latest: Mar 30 2021 at 20:03)
- Cardinality of quotient β€ (7 messages, latest: Mar 30 2021 at 18:20)
- Rank of a linear map is lower semi continuous (8 messages, latest: Mar 30 2021 at 05:27)
- axiom of choice for finite collections? (5 messages, latest: Mar 29 2021 at 20:10)
- Transporting
mul_action
along 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) - nat.log_mono (7 messages, latest: Mar 26 2021 at 20:49)
- better/best solving AI? (39 messages, latest: Mar 26 2021 at 09:09)
injective.map_swap
(4 messages, latest: Mar 25 2021 at 17:15)- fin.rotate (57 messages, latest: Mar 24 2021 at 17:40)
- gcd_nsmul_eq_zero? (4 messages, latest: Mar 23 2021 at 08:20)
- left_inverse imples ` Ξ± β set.range f` (2 messages, latest: Mar 22 2021 at 18:09)
- group_with_zero morphisms with domain β (37 messages, latest: Mar 21 2021 at 21:36)
- nodup vs. count vs length (7 messages, latest: Mar 21 2021 at 00:21)
- Injectivity of field extensions (4 messages, latest: Mar 20 2021 at 20:46)
- frequently_in_nhds_map (24 messages, latest: Mar 20 2021 at 03:46)
- structure theorem for finite boolean algebras (7 messages, latest: Mar 19 2021 at 18:59)
no_zero_divisors
instance on polynomials? (6 messages, latest: Mar 19 2021 at 08:45)- mul_neg (8 messages, latest: Mar 19 2021 at 06:57)
- Cancelling in a domain (3 messages, latest: Mar 19 2021 at 06:17)
- line_map (4 messages, latest: Mar 19 2021 at 03:36)
- group.div_self (7 messages, latest: Mar 18 2021 at 12:05)
- Projective R-modules. (44 messages, latest: Mar 17 2021 at 23:19)
- algebraic structures on lists (4 messages, latest: Mar 17 2021 at 16:46)
- singleton embedding (4 messages, latest: Mar 17 2021 at 16:42)
- subsingleton from card = 1 (3 messages, latest: Mar 16 2021 at 16:11)
- IMO 2012-4 (3 messages, latest: Mar 16 2021 at 15:14)
- is_square/is_power (29 messages, latest: Mar 16 2021 at 14:44)
- continuous_sup (12 messages, latest: Mar 16 2021 at 10:57)
- sup norm on continuous functions? (31 messages, latest: Mar 16 2021 at 01:03)
- (continous) linear_maps between
p
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)
- Sums and products with multiplicative/additive (3 messages, latest: Mar 14 2021 at 14:59)
- Matrix on edge set for graphs (51 messages, latest: Mar 12 2021 at 19:45)
finsupp.single (f x) y (f z) = finsupp.single x y z
(2 messages, latest: Mar 12 2021 at 16:11)- poly (a)eval and algebra maps (13 messages, latest: Mar 11 2021 at 19:32)
- Cokers of morphisms of add_comm_groups (5 messages, latest: Mar 11 2021 at 07:30)
- succ_succ_ne_one (27 messages, latest: Mar 11 2021 at 06:13)
- Correct setting for positive shifts of intervals (37 messages, latest: Mar 10 2021 at 20:27)
- list.update_nth_same (9 messages, latest: Mar 10 2021 at 13:49)
- le on option (5 messages, latest: Mar 09 2021 at 19:30)
- Bilinear form on
finsupp
(6 messages, latest: Mar 09 2021 at 18:25) - Reduce like operation for finite sets (14 messages, latest: Mar 08 2021 at 22:58)
- add_sub_swap (5 messages, latest: Mar 08 2021 at 12:28)
- generators smul generators generate (76 messages, latest: Mar 07 2021 at 15:08)
- affine span is convex (6 messages, latest: Mar 06 2021 at 23:20)
- G-module maps (20 messages, latest: Mar 06 2021 at 20:03)
- Sum is linear (19 messages, latest: Mar 06 2021 at 18:53)
- list.update_same (2 messages, latest: Mar 04 2021 at 13:47)
- le_or_le (7 messages, latest: Mar 04 2021 at 07:55)
- functor.comp as a functor (3 messages, latest: Mar 03 2021 at 21:06)
- Is there a
ring
instance on a semiring that is a β€-algeβ¦ (9 messages, latest: Mar 03 2021 at 08:47) - ne of mem and not mem (12 messages, latest: Mar 03 2021 at 03:47)
- topology without filters (3 messages, latest: Mar 02 2021 at 05:11)
- Category of diagrams (5 messages, latest: Mar 01 2021 at 23:25)
- linear image of segment (5 messages, latest: Mar 01 2021 at 23:09)
- linear map to matrices, ring_equiv (41 messages, latest: Mar 01 2021 at 19:35)
- classicalize (80 messages, latest: Mar 01 2021 at 10:04)
- inequality involving
/2
(6 messages, latest: Mar 01 2021 at 07:32) - "Reversing"
fin
(10 messages, latest: Feb 28 2021 at 12:25) - Filter golf (83 messages, latest: Feb 27 2021 at 16:44)
- A
strict_mono
function fromβ
is determined by its image (3 messages, latest: Feb 27 2021 at 16:22) - nonempty linear_order (4 messages, latest: Feb 27 2021 at 08:38)
- measure theory for algebraists (8 messages, latest: Feb 26 2021 at 21:56)
- constructing
subalgebra
without duplicate axioms (2 messages, latest: Feb 25 2021 at 19:40) - Chauchy-Schwarz (9 messages, latest: Feb 24 2021 at 18:11)
- Transitive symmetric relations (12 messages, latest: Feb 24 2021 at 13:17)
- mem_span_of_mem_span (11 messages, latest: Feb 23 2021 at 13:07)
- well-founded linear order on a type (3 messages, latest: Feb 22 2021 at 22:13)
- Unfolding let bindings in hypotheses (81 messages, latest: Feb 22 2021 at 18:17)
- Finiteness of balls in the integers (5 messages, latest: Feb 22 2021 at 14:28)
- linear maps in the constructor for power_series (6 messages, latest: Feb 22 2021 at 13:34)
- Order from embedding (50 messages, latest: Feb 21 2021 at 17:21)
- Integrals on [0, +inf] as limits (1 message, latest: Feb 20 2021 at 23:10)
- A typeclass for nat subtraction (18 messages, latest: Feb 20 2021 at 18:41)
- int.iterate (8 messages, latest: Feb 20 2021 at 17:10)
- functors and universe constraints (10 messages, latest: Feb 20 2021 at 09:35)
- distinct (14 messages, latest: Feb 19 2021 at 19:31)
- Linear indep of nonzero smul (1 message, latest: Feb 19 2021 at 17:31)
- General lift (5 messages, latest: Feb 19 2021 at 16:51)
- Simple integral calculations (27 messages, latest: Feb 19 2021 at 08:53)
- by_cases foo, {finish} (9 messages, latest: Feb 18 2021 at 22:31)
- nontrivial matrices (6 messages, latest: Feb 18 2021 at 17:13)
- Converting from one type to another (15 messages, latest: Feb 18 2021 at 15:29)
integral_restrict
(20 messages, latest: Feb 18 2021 at 12:53)- assume h and then prove cases for h and not h (11 messages, latest: Feb 18 2021 at 10:37)
- list.nth is either none (5 messages, latest: Feb 16 2021 at 19:29)
- set.erase (3 messages, latest: Feb 16 2021 at 17:57)
- complement of finite in infinite is infinite (21 messages, latest: Feb 16 2021 at 17:39)
- monotone increasing or decreasing subsequence (11 messages, latest: Feb 16 2021 at 02:59)
- additive functors (8 messages, latest: Feb 16 2021 at 02:01)
- Krull dimension, regular rings (8 messages, latest: Feb 15 2021 at 11:56)
- not_mem lemmas (4 messages, latest: Feb 15 2021 at 06:55)
- Injective map inducing perm group homomorphism (2 messages, latest: Feb 15 2021 at 04:15)
- range with step (7 messages, latest: Feb 14 2021 at 17:54)
- different gcd's? (16 messages, latest: Feb 13 2021 at 01:57)
- linear maps (4 messages, latest: Feb 11 2021 at 11:05)
- Homomorphism estensionnality (7 messages, latest: Feb 11 2021 at 09:39)
- lt_of_add_lt (9 messages, latest: Feb 11 2021 at 08:21)
- First isomorphism theorem for rings (33 messages, latest: Feb 11 2021 at 06:48)
- discrete bot (2 messages, latest: Feb 10 2021 at 21:36)
- fintype_of_univ_finite (2 messages, latest: Feb 10 2021 at 21:36)
- primes associated of dvd (20 messages, latest: Feb 10 2021 at 19:33)
- Special cases of Fermat's Last Theorem (10 messages, latest: Feb 10 2021 at 11:28)
- powers are monotone in the base (6 messages, latest: Feb 10 2021 at 06:42)
- prime generator of prime ideal (3 messages, latest: Feb 09 2021 at 10:19)
- Membership in Sup of submodules (7 messages, latest: Feb 09 2021 at 03:47)
- linear map of subspace ne top (12 messages, latest: Feb 06 2021 at 02:45)
- P-adic valuation on polynomials (21 messages, latest: Feb 05 2021 at 15:41)
- evaluation map from sets to sets (16 messages, latest: Feb 03 2021 at 23:07)
- Halves of a sorted list are related (52 messages, latest: Feb 03 2021 at 19:14)
- lifting sub from Q to N? (6 messages, latest: Feb 03 2021 at 17:45)
- lt on functions (2 messages, latest: Feb 03 2021 at 14:37)
- tsum_lt? (39 messages, latest: Feb 03 2021 at 14:24)
- nat.find_ge_of_not? (5 messages, latest: Feb 03 2021 at 00:04)
- real.log_ne_zero_iff? (25 messages, latest: Feb 02 2021 at 13:23)
- Swapping quotients (2 messages, latest: Feb 02 2021 at 04:35)
- Semifields? (53 messages, latest: Feb 01 2021 at 21:27)
- Quotient thing (7 messages, latest: Feb 01 2021 at 16:28)
- exists_unique from equiv (17 messages, latest: Feb 01 2021 at 12:36)
- induction on n where n β 0 (32 messages, latest: Feb 01 2021 at 06:30)
int
in other universes (9 messages, latest: Jan 31 2021 at 21:41)norm
as a quadratic form (6 messages, latest: Jan 31 2021 at 18:26)- saturated submonoids, kernels and beyond (25 messages, latest: Jan 31 2021 at 17:51)
- degree_prod (22 messages, latest: Jan 31 2021 at 07:30)
- condition on type class (5 messages, latest: Jan 30 2021 at 22:42)
- Bezout (12 messages, latest: Jan 30 2021 at 00:56)
- Inverse
finset.product
(12 messages, latest: Jan 29 2021 at 17:24) - Get single element from
finset
(10 messages, latest: Jan 29 2021 at 15:14) - Is there a definition of a Z-module nZ for any n? (7 messages, latest: Jan 29 2021 at 14:19)
- "classical" definition of limit of sequence (5 messages, latest: Jan 29 2021 at 01:50)
- holomorphic functions on the upper half plane (18 messages, latest: Jan 27 2021 at 15:05)
- Liquid Tensor Experiment (3 messages, latest: Jan 25 2021 at 07:07)
- Bilattices (16 messages, latest: Jan 23 2021 at 17:54)
- finite_dimensional_of_findim_pos (2 messages, latest: Jan 22 2021 at 19:15)
- cardinal.pos_of_one_le (10 messages, latest: Jan 22 2021 at 16:49)
- CW Complex (6 messages, latest: Jan 22 2021 at 11:43)
- matrix.dot_product is a linear map (5 messages, latest: Jan 22 2021 at 09:30)
- Application of
add_monoid_hom
distributes 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)
- 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)
- S1 and other topological spaces (37 messages, latest: Sep 22 2020 at 23:58)
- Fibered products (7 messages, latest: Sep 22 2020 at 21:34)
- auto-coercions (24 messages, latest: Sep 21 2020 at 21:46)
- Gcd type tags (14 messages, latest: Sep 21 2020 at 21:18)
- Functor preserving binary products (13 messages, latest: Sep 21 2020 at 15:08)
- monad question (14 messages, latest: Sep 20 2020 at 05:34)
- Copying projections through a definition (2 messages, latest: Sep 17 2020 at 18:31)
rw
part of an inequality (14 messages, latest: Sep 16 2020 at 15:00)- cast_card_eq_zero (1 message, latest: Sep 16 2020 at 09:21)
- nat.pow_pos (5 messages, latest: Sep 15 2020 at 19:23)
- implication on
bool
(5 messages, latest: Sep 15 2020 at 14:49) - suppress an hyptohesis (12 messages, latest: Sep 15 2020 at 08:44)
- Setoid associated to filter (15 messages, latest: Sep 14 2020 at 20:34)
- Multiset to set (42 messages, latest: Sep 14 2020 at 09:49)
- how do I activate
sum.lex
? (3 messages, latest: Sep 14 2020 at 08:57) - sq_sub_sq for nat (8 messages, latest: Sep 13 2020 at 21:29)
- Tail of bounded series tends to zero (2 messages, latest: Sep 12 2020 at 20:15)
- Subalgebras over different base fields (4 messages, latest: Sep 10 2020 at 22:49)
- continuous map to \top (3 messages, latest: Sep 10 2020 at 17:27)
- nat.rec_succ (5 messages, latest: Sep 10 2020 at 14:21)
- base change of module (20 messages, latest: Sep 09 2020 at 20:57)
- R is the unique complete archimedean ordered field (7 messages, latest: Sep 08 2020 at 16:49)
- Coprime numbers whose product is a square are both square (8 messages, latest: Sep 08 2020 at 16:13)
- Mapping ideals to localizations (3 messages, latest: Sep 07 2020 at 15:42)
- associates R -> ideal R (1 message, latest: Sep 06 2020 at 16:59)
- single-valued relation (2 messages, latest: Sep 06 2020 at 15:57)
at_top
for an interval (8 messages, latest: Sep 04 2020 at 23:15)- comp_apply for concrete categories (3 messages, latest: Sep 04 2020 at 13:06)
- Fermat's right triangle theorem (9 messages, latest: Sep 04 2020 at 08:39)
- linear dependence of more than dimension (46 messages, latest: Sep 03 2020 at 10:19)
- fincard X^Y (2 messages, latest: Sep 03 2020 at 04:51)
- p-adic integers as inverse limit (7 messages, latest: Sep 02 2020 at 14:30)
- I-adic valuation on R (18 messages, latest: Sep 02 2020 at 13:17)
- if f o g is linearly independent then so is g (2 messages, latest: Sep 01 2020 at 15:50)
- Galois fields or Elliptic curves? (6 messages, latest: Sep 01 2020 at 12:14)
- vector.prod (2 messages, latest: Sep 01 2020 at 11:57)
- localization away from f (5 messages, latest: Sep 01 2020 at 03:32)
fintype.induction_on
(32 messages, latest: Aug 29 2020 at 19:43)- has_mem for subgroups of units (10 messages, latest: Aug 27 2020 at 19:57)
- pull back an R module along
S ->+* R
(35 messages, latest: Aug 26 2020 at 12:33) - line break in tactic.pp (5 messages, latest: Aug 26 2020 at 12:25)
- integral and linear maps (1 message, latest: Aug 25 2020 at 22:10)
- apply linear_map (1 message, latest: Aug 25 2020 at 21:14)
- infinite sums of functions (10 messages, latest: Aug 25 2020 at 20:48)
- finsupp gsmul_eq_smul (9 messages, latest: Aug 25 2020 at 17:55)
- Transfer instance through equivalences (11 messages, latest: Aug 25 2020 at 11:58)
- Category instance on Sigma type (3 messages, latest: Aug 24 2020 at 23:06)
- Status of Spectral Theorem? (109 messages, latest: Aug 24 2020 at 21:57)
- rewrite at a specific variable? (10 messages, latest: Aug 24 2020 at 20:00)
- quotient by product relation (16 messages, latest: Aug 24 2020 at 19:58)
- Pythagoras' Theorem (3 messages, latest: Aug 23 2020 at 17:02)
- "Archimedean minimal" (3 messages, latest: Aug 21 2020 at 22:24)
multiset.nodup s β β a t, s β a :: a :: t
(3 messages, latest: Aug 20 2020 at 07:07)- Hyperbolic Trig Functions (18 messages, latest: Aug 18 2020 at 11:02)
- Set coercion (8 messages, latest: Aug 17 2020 at 20:18)
- Order topology (17 messages, latest: Aug 17 2020 at 18:57)
- category of POSet (12 messages, latest: Aug 17 2020 at 17:27)
- Gram-Schmidt orthogonalization (28 messages, latest: Aug 16 2020 at 19:14)
- Krull's Theorem (5 messages, latest: Aug 16 2020 at 17:17)
- category of sets (17 messages, latest: Aug 15 2020 at 13:19)
- maximal ideals in integral extensions (5 messages, latest: Aug 15 2020 at 09:31)
- fintype.equiv_congr (19 messages, latest: Aug 15 2020 at 05:05)
- Isomorphisms of categories (16 messages, latest: Aug 14 2020 at 22:44)
- Ordered groups have no top element (8 messages, latest: Aug 14 2020 at 20:15)
- fast div and mod (5 messages, latest: Aug 12 2020 at 15:51)
- Iterated product is multilinear (2 messages, latest: Aug 12 2020 at 15:39)
- initial / final functors (5 messages, latest: Aug 12 2020 at 13:33)
- Left and right inverse of function (2 messages, latest: Aug 12 2020 at 00:50)
- Morphisms of monads (72 messages, latest: Aug 11 2020 at 22:59)
- Predicates on predicates involving instances (4 messages, latest: Aug 10 2020 at 07:43)
- polynomial comp and map (7 messages, latest: Aug 10 2020 at 06:45)
linear_order
compatible with a 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)- use mathlib branch in project (5 messages, latest: Aug 05 2020 at 00:55)
- Ideals over algebras (139 messages, latest: Aug 04 2020 at 18:06)
- Distrib lattice constructors (4 messages, latest: Aug 03 2020 at 05:46)
- Big op products with rearranged indices (3 messages, latest: Aug 02 2020 at 13:07)
- Finite dimensional vector space over a finite field (28 messages, latest: Jul 30 2020 at 18:31)
- manipulating multiset elements in proof (10 messages, latest: Jul 29 2020 at 18:20)
- Sheaves of category-objects (68 messages, latest: Jul 29 2020 at 16:57)
- reverse β take = drop β reverse (10 messages, latest: Jul 28 2020 at 13:46)
- union of list of finsets (18 messages, latest: Jul 28 2020 at 08:53)
- (list.cons a l) β l (35 messages, latest: Jul 27 2020 at 19:11)
- a lemma about βinducingβ open_embedding? (1 message, latest: Jul 27 2020 at 13:59)
- a lemma about inducing? (16 messages, latest: Jul 27 2020 at 13:51)
- mul_linear_map (7 messages, latest: Jul 27 2020 at 09:31)
- Tangent Space of Sphere (1 message, latest: Jul 26 2020 at 17:36)
- Automating over structures (6 messages, latest: Jul 25 2020 at 04:29)
- monoid object (18 messages, latest: Jul 25 2020 at 02:56)
- std_basis (3 messages, latest: Jul 24 2020 at 20:45)
- Right inverse of injective (3 messages, latest: Jul 24 2020 at 17:34)
- mulabel (3 messages, latest: Jul 23 2020 at 09:11)
- dfinsupp of product is dfinsupp of dfinsupp (13 messages, latest: Jul 22 2020 at 12:14)
- locally ringed spaces (1 message, latest: Jul 22 2020 at 09:27)
- Local vs global minimum (17 messages, latest: Jul 20 2020 at 02:58)
- decidable search on a list (5 messages, latest: Jul 19 2020 at 15:54)
- int.coe_to_nat_eq (4 messages, latest: Jul 19 2020 at 11:29)
- symmetric.iff (3 messages, latest: Jul 19 2020 at 05:07)
- All but last element of a list (8 messages, latest: Jul 18 2020 at 18:54)
- Linear combinations stay in a submodule (10 messages, latest: Jul 18 2020 at 17:32)
- Z/nZ = zmod? (1 message, latest: Jul 18 2020 at 10:59)
- fderiv is 0 if derivative is 0 (8 messages, latest: Jul 15 2020 at 21:12)
- Automatic intro/cases/specialize/use dance (31 messages, latest: Jul 15 2020 at 19:25)
- recovering from an
exists
(11 messages, latest: Jul 13 2020 at 01:06) - finite fields (41 messages, latest: Jul 11 2020 at 06:29)
- How best to express my applied maths problem in mathlib? (5 messages, latest: Jul 10 2020 at 13:47)
- Disjoint union of fin's (6 messages, latest: Jul 10 2020 at 00:42)
- quotient by bottom setoid (5 messages, latest: Jul 09 2020 at 19:12)
- is_unit_group (4 messages, latest: Jul 09 2020 at 10:27)
- Apply function N times (23 messages, latest: Jul 07 2020 at 20:51)
- list (option Ξ±) β list Ξ± (27 messages, latest: Jul 07 2020 at 19:47)
- list.split_sum (7 messages, latest: Jul 07 2020 at 19:47)
- list operation (9 messages, latest: Jul 05 2020 at 18:08)
- sum_sum_elim for fintypes (16 messages, latest: Jul 05 2020 at 17:07)
- Lean, show me the first 5 elements in the set of natural num (10 messages, latest: Jul 04 2020 at 20:11)
- add_monoid_hom.cod_restrict (1 message, latest: Jul 04 2020 at 19:27)
- bundled one-sided invertible functions (7 messages, latest: Jul 02 2020 at 14:22)
- Doing differential geometry (10 messages, latest: Jul 01 2020 at 03:11)
- A boolean algebra is an ordered comm monoid (15 messages, latest: Jun 30 2020 at 06:49)
- Finite geometric series (43 messages, latest: Jun 29 2020 at 03:01)
- isomorphisms define category (3 messages, latest: Jun 29 2020 at 00:27)
- nonzero (fin n.succ.succ) (8 messages, latest: Jun 28 2020 at 23:01)
- Statement of Cauchy's integral formula (4 messages, latest: Jun 28 2020 at 04:22)
- Rigs and rings (2 messages, latest: Jun 28 2020 at 04:14)
- Equal within s imply same limit within s (65 messages, latest: Jun 27 2020 at 20:14)
- telescoping sums (35 messages, latest: Jun 26 2020 at 13:37)
- Redefining Operators (21 messages, latest: Jun 26 2020 at 03:24)
- Injective on a set up to a relation (10 messages, latest: Jun 25 2020 at 19:45)
- Is there code for Galois theory? (60 messages, latest: Jun 24 2020 at 08:47)
- Decompose a natural into perfect square (4 messages, latest: Jun 23 2020 at 23:36)
- fdvs lemmas (23 messages, latest: Jun 23 2020 at 00:38)
- finsupp tensor finsupp (8 messages, latest: Jun 22 2020 at 23:59)
- finsupp is direct sum (6 messages, latest: Jun 22 2020 at 23:50)
- Results on gcd (8 messages, latest: Jun 20 2020 at 22:32)
- prod_ite_eq (11 messages, latest: Jun 18 2020 at 15:14)
- Cartesian Closed Categories (6 messages, latest: Jun 16 2020 at 03:50)
- order on bool (11 messages, latest: Jun 15 2020 at 01:01)
- pretty printing an expr (4 messages, latest: Jun 14 2020 at 16:05)
- add_comm_group tactic? (19 messages, latest: Jun 14 2020 at 04:05)
- Usual topology on R (6 messages, latest: Jun 12 2020 at 13:42)
- if the dual of a well order is also a well order then finite (13 messages, latest: Jun 11 2020 at 08:06)
- a well-ordered subset of \R is countable (4 messages, latest: Jun 11 2020 at 07:56)
- Linear combination description of span (3 messages, latest: Jun 10 2020 at 21:58)
- A finite division ring is a field (11 messages, latest: Jun 09 2020 at 07:01)
0 β€ x * x + y * y
again (14 messages, latest: Jun 08 2020 at 15:11)- Identify span of vector with field (12 messages, latest: Jun 08 2020 at 05:08)
- Preimage of finite sets (32 messages, latest: Jun 06 2020 at 20:19)
- f(x)=q(x)(x-r) + f(r) (16 messages, latest: Jun 02 2020 at 19:45)
- has_mem for subtype (23 messages, latest: Jun 02 2020 at 14:00)
- trunc (14 messages, latest: Jun 02 2020 at 06:22)
- 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)
- Ideals of an algebra are submodules (16 messages, latest: May 14 2020 at 14:33)
- List lemmas (14 messages, latest: May 12 2020 at 10:40)
- sequence tending to a limit (10 messages, latest: May 10 2020 at 18:38)
- subtype.property' (2 messages, latest: May 06 2020 at 13:18)
- basis of free module
X -> R
with [fintype X]? (4 messages, latest: May 02 2020 at 12:08) - projectors (13 messages, latest: Apr 30 2020 at 23:27)
- real powers of positive reals? (17 messages, latest: Apr 30 2020 at 15:01)
- bnot (a && b) = (bnot a) || (bnot b) (27 messages, latest: Apr 25 2020 at 19:48)
- exporting a program's AST (10 messages, latest: Apr 25 2020 at 02:25)
- enumerating a fintype (6 messages, latest: Apr 23 2020 at 05:21)
- last n elements of a list (10 messages, latest: Apr 21 2020 at 09:35)
- continuous functions commute with limits? (15 messages, latest: Apr 19 2020 at 19:25)
- list.is_palindrome (6 messages, latest: Apr 19 2020 at 00:11)
- Density of Q in R (8 messages, latest: Apr 17 2020 at 13:11)
- nat.eq_div_of_mul_eq (44 messages, latest: Apr 16 2020 at 14:24)
- undergraduate calculus (81 messages, latest: Apr 15 2020 at 12:18)
- algebra R (monoid_algebra R G) (21 messages, latest: Apr 15 2020 at 01:40)
- definite and indefinite integrals on the reals (7 messages, latest: Apr 14 2020 at 19:18)
- Bolzano-Weirstrass (89 messages, latest: Apr 12 2020 at 11:33)
- fintype (s.to_set) (6 messages, latest: Apr 12 2020 at 10:54)
- add_left_cancel_monoid (16 messages, latest: Apr 10 2020 at 07:43)
- high scores (24 messages, latest: Apr 05 2020 at 12:04)
- Multiplicative group of integers modulo n (12 messages, latest: Mar 15 2020 at 02:54)
- Sorted set (2 messages, latest: Mar 01 2020 at 10:06)
- If there is an inverse, it's unique? (2 messages, latest: Feb 26 2020 at 11:30)
- distance preserving maps (12 messages, latest: Feb 24 2020 at 19:48)
- General linear groups (3 messages, latest: Feb 21 2020 at 23:20)
- smul_comm (1 message, latest: Feb 10 2020 at 18:59)
- mem_span if finite linear combination (4 messages, latest: Feb 10 2020 at 09:56)
- Getting instance from parent instance (2 messages, latest: Feb 09 2020 at 15:59)
- representation theory of finite groups (4 messages, latest: Jan 17 2020 at 05:52)
- the trace of a square matrix (1 message, latest: Jan 15 2020 at 22:44)
- valuation rings (3 messages, latest: Dec 30 2019 at 09:15)
- Completion of a ring (2 messages, latest: Dec 23 2019 at 15:38)
- Super vector space (1 message, latest: Dec 22 2019 at 14:10)
Last updated: Jan 31 2023 at 21:29 UTC