Zulip Chat Archive
Stream: FLT regular
Topics:
- blueprint (86 messages, latest: Jan 31 2023 at 15:07)
- lean4 (14 messages, latest: Jan 11 2023 at 17:18)
- leanproject up (13 messages, latest: Dec 26 2022 at 19:42)
- Project status (180 messages, latest: Nov 21 2022 at 16:33)
- homogenization.lean (10 messages, latest: Nov 09 2022 at 07:03)
- Case II (2 messages, latest: Oct 17 2022 at 17:08)
- End of caseI (72 messages, latest: Oct 14 2022 at 15:59)
- Case I (210 messages, latest: Oct 12 2022 at 16:38)
- Exponent 3 (11 messages, latest: Oct 03 2022 at 12:37)
- mem_roots_of_unity_of_abs_eq_one (68 messages, latest: Oct 02 2022 at 13:11)
- A paper mentioning formalizing FLT regular (4 messages, latest: Sep 06 2022 at 09:19)
- instances (23 messages, latest: Jul 15 2022 at 14:09)
- Contributing to the project (281 messages, latest: Jul 11 2022 at 11:56)
- ne_zero again (23 messages, latest: Jun 20 2022 at 07:51)
- unit_lemma (9 messages, latest: Jun 10 2022 at 13:50)
- dependency graph (15 messages, latest: Jun 03 2022 at 13:18)
- [hn : (↑n : ) ≠ 0](topic/hn.20.3A.20(.E2.86.91n.20.3A.20).20.E2.89.A0.200.html) (65 messages, latest: May 10 2022 at 20:19)
- Mathlib bump (72 messages, latest: May 02 2022 at 10:50)
- Discriminant of p^n-th cyclotomic field (21 messages, latest: Apr 25 2022 at 11:42)
- Deploy error (31 messages, latest: Apr 15 2022 at 08:42)
- Project update (11 messages, latest: Mar 29 2022 at 05:04)
- Power basis (14 messages, latest: Feb 23 2022 at 17:10)
- Unit lemma (14 messages, latest: Feb 11 2022 at 13:18)
- zeta PR (16 messages, latest: Feb 09 2022 at 20:05)
- galois stuff (19 messages, latest: Feb 08 2022 at 17:33)
- Kummer's lemma (66 messages, latest: Feb 05 2022 at 19:17)
- zeta and primitive roots (8 messages, latest: Feb 03 2022 at 17:42)
- Cyclotomic field defn (432 messages, latest: Feb 01 2022 at 00:56)
- lean projects board (10 messages, latest: Jan 21 2022 at 16:47)
- zeta vs zeta' (72 messages, latest: Jan 11 2022 at 17:16)
- Further properties of the discriminant (23 messages, latest: Jan 11 2022 at 09:07)
- Intervals in fin n (29 messages, latest: Dec 27 2021 at 14:36)
- Cleanup (2 messages, latest: Dec 23 2021 at 21:10)
- Discriminant (155 messages, latest: Dec 23 2021 at 09:37)
- Factorizations (1 message, latest: Nov 29 2021 at 20:23)
- finite_dimensional instance (20 messages, latest: Nov 17 2021 at 14:13)
- Cyclotomic units (45 messages, latest: Nov 10 2021 at 15:12)
- docstrings (9 messages, latest: Nov 10 2021 at 00:04)
roots_equal_embeddings(5 messages, latest: Nov 09 2021 at 20:09)- may_assume and instances (4 messages, latest: Nov 09 2021 at 00:17)
- Embeddings (27 messages, latest: Nov 05 2021 at 10:39)
- ready_for_mathlib (10 messages, latest: Nov 03 2021 at 09:56)
- Kronecker (12 messages, latest: Nov 01 2021 at 23:25)
- gitpod (6 messages, latest: Oct 29 2021 at 12:59)
- General notation (5 messages, latest: Oct 28 2021 at 14:26)
- stream events (4 messages, latest: Oct 25 2021 at 16:39)
Last updated: Jan 31 2023 at 21:29 UTC