Zulip Chat Archive

Stream: FLT-regular

Topic: Cleanup

Riccardo Brasca (Dec 23 2021 at 19:31):

@Eric Rodriguez When you have time, can you have a look at src/ready_for_mathlib/cyclotomic.lean? Do we need the results there or are there already in mathlib/PRed?

Eric Rodriguez (Dec 23 2021 at 21:10):

omw!

Riccardo Brasca (Dec 23 2021 at 19:31):

@Eric Rodriguez When you have time, can you have a look at src/ready_for_mathlib/cyclotomic.lean? Do we need the results there or are there already in mathlib/PRed?

Eric Rodriguez (Dec 23 2021 at 21:10):

omw!

Last updated: May 02 2025 at 03:31 UTC