English
Equivalent expression of the previous node-derivative relation.
Русский
То же самое в другой формулировке о связи производной и узла.
LaTeX
$$$ \\text{(same as previous)} $$$
Lean4
/-- The vanishing polynomial on a multiplicative subgroup is of the form X ^ n - 1. -/
@[simp]
theorem nodal_subgroup_eq_X_pow_card_sub_one [IsDomain R] (G : Subgroup Rˣ) [Fintype G] :
nodal (G : Set Rˣ).toFinset ((↑) : Rˣ → R) = X ^ (Fintype.card G) - 1 :=
by
have h : degree (1 : R[X]) < degree ((X : R[X]) ^ Fintype.card G) := by simp [Fintype.card_pos]
apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
· exact Units.val_injective.injOn
· simp
· rw [degree_sub_eq_left_of_degree_lt h, degree_nodal, Set.toFinset_card, degree_pow, degree_X, nsmul_eq_mul, mul_one,
Nat.cast_inj]
exact rfl
· rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]
· intro i hi
rw [eval_nodal_at_node hi]
replace hi : i ∈ G := by simpa using hi
obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩
simp [← Units.val_pow_eq_pow_val, ← Subgroup.coe_pow G]
