noncomputable def Domain.CosetFftDomainClass.toList {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) : List ↥(toFinset ω)

theorem Domain.CosetFftDomainClass.toList_eq_finset_toList {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} : List.map (fun (x : ↥(toFinset ω)) => ↑x) (toList ω) = (toFinset ω).toList

def Domain.CosetFftDomain.toList {F : Type} [Field F] [DecidableEq F] {m : ℕ} [NeZero m] (ω : CosetFftDomain (Fin m) F) : List ↥ω.toFinset

Convert a coset FFT domain into a list of all its members with proofs the members belong to the FFT domain.

Computable for FFT domains indexed by Fin m, by enumerating via List.finRange m.

def Domain.FftDomain.toList {F : Type} [Field F] [DecidableEq F] {m : ℕ} [NeZero m] (ω : FftDomain (Fin m) F) : List ↥ω.toFinset

Convert a FFT domain into a list of all its members with proofs the members belong to the FFT domain.

Computable for FFT domains indexed by Fin m, by enumerating via List.finRange m.