Zulip Chat Archive
Stream: FLT-regular
Topics:
- Mathlib bumps (139 messages, latest: Jun 13 2025 at 20:18)
- homogenization.lean (32 messages, latest: Jul 25 2024 at 11:08)
- flt3 (2 messages, latest: Jul 16 2024 at 09:47)
- channel events (1 message, latest: Jun 21 2024 at 01:35)
- graph (8 messages, latest: Apr 28 2024 at 12:26)
- Future work (45 messages, latest: Mar 12 2024 at 16:26)
- Mathlib PRs (29 messages, latest: Jan 06 2024 at 22:24)
- Mathlib bump (148 messages, latest: Dec 18 2023 at 11:44)
- Ramification (7 messages, latest: Dec 17 2023 at 21:09)
- This stream is not world-readable (10 messages, latest: Dec 07 2023 at 07:37)
- stream events (19 messages, latest: Dec 07 2023 at 07:36)
- Completion of FLT-regular (8 messages, latest: Dec 05 2023 at 14:49)
- Kummer's lemma (270 messages, latest: Dec 02 2023 at 16:27)
- FLT and the binomial theorem (1 message, latest: Nov 30 2023 at 00:16)
- blueprint (277 messages, latest: Nov 06 2023 at 18:55)
- Golfing (6 messages, latest: Nov 06 2023 at 17:24)
- Jacquet-Langlands/base change (10 messages, latest: Oct 14 2023 at 16:01)
- Case II (26 messages, latest: Oct 02 2023 at 10:42)
- gen_dvd_by_frak_p (11 messages, latest: Sep 26 2023 at 14:40)
- Port to Lean4 (36 messages, latest: Sep 09 2023 at 19:17)
- Project status (361 messages, latest: May 23 2023 at 14:59)
- lean4 (45 messages, latest: Apr 04 2023 at 13:22)
- leanproject up (26 messages, latest: Dec 26 2022 at 19:42)
- End of caseI (144 messages, latest: Oct 14 2022 at 15:59)
- Case I (420 messages, latest: Oct 12 2022 at 16:38)
- Exponent 3 (22 messages, latest: Oct 03 2022 at 12:37)
- mem_roots_of_unity_of_abs_eq_one (136 messages, latest: Oct 02 2022 at 13:11)
- A paper mentioning formalizing FLT regular (8 messages, latest: Sep 06 2022 at 09:19)
- instances (46 messages, latest: Jul 15 2022 at 14:09)
- Contributing to the project (562 messages, latest: Jul 11 2022 at 11:56)
- ne_zero again (46 messages, latest: Jun 20 2022 at 07:51)
- unit_lemma (18 messages, latest: Jun 10 2022 at 13:50)
- dependency graph (30 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) (130 messages, latest: May 10 2022 at 20:19)
- Discriminant of p^n-th cyclotomic field (42 messages, latest: Apr 25 2022 at 11:42)
- Deploy error (62 messages, latest: Apr 15 2022 at 08:42)
- Project update (22 messages, latest: Mar 29 2022 at 05:04)
- Power basis (28 messages, latest: Feb 23 2022 at 17:10)
- Unit lemma (28 messages, latest: Feb 11 2022 at 13:18)
- zeta PR (32 messages, latest: Feb 09 2022 at 20:05)
- galois stuff (38 messages, latest: Feb 08 2022 at 17:33)
- zeta and primitive roots (16 messages, latest: Feb 03 2022 at 17:42)
- Cyclotomic field defn (864 messages, latest: Feb 01 2022 at 00:56)
- lean projects board (20 messages, latest: Jan 21 2022 at 16:47)
- zeta vs zeta' (144 messages, latest: Jan 11 2022 at 17:16)
- Further properties of the discriminant (46 messages, latest: Jan 11 2022 at 09:07)
- Intervals in fin n (58 messages, latest: Dec 27 2021 at 14:36)
- Cleanup (4 messages, latest: Dec 23 2021 at 21:10)
- Discriminant (310 messages, latest: Dec 23 2021 at 09:37)
- Factorizations (2 messages, latest: Nov 29 2021 at 20:23)
- finite_dimensional instance (40 messages, latest: Nov 17 2021 at 14:13)
- Cyclotomic units (90 messages, latest: Nov 10 2021 at 15:12)
- docstrings (18 messages, latest: Nov 10 2021 at 00:04)
roots_equal_embeddings(10 messages, latest: Nov 09 2021 at 20:09)- may_assume and instances (8 messages, latest: Nov 09 2021 at 00:17)
- Embeddings (54 messages, latest: Nov 05 2021 at 10:39)
- ready_for_mathlib (20 messages, latest: Nov 03 2021 at 09:56)
- Kronecker (24 messages, latest: Nov 01 2021 at 23:25)
- gitpod (12 messages, latest: Oct 29 2021 at 12:59)
- General notation (10 messages, latest: Oct 28 2021 at 14:26)
Last updated: Feb 28 2026 at 14:05 UTC