proposition: Lemma Cyclotomic1 : 'Phi_1 = 'X - 1.
proof: Proof. by have := @prod_Cyclotomic 1%N isT; rewrite big_cons big_nil mulr1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)