English
For a fixed point x in F, the minimal polynomial of x over FixedPoints.subfield G F is monic.
Русский
Для фиксированной точки x в F минимальный многочлен над FixedPoints.subfield G F мономиален.
LaTeX
$$$ (FixedPoints.minpoly G F x).Monic $$$
Lean4
theorem linearIndependent_smul_of_linearIndependent {s : Finset F} :
(LinearIndepOn (FixedPoints.subfield G F) id (s : Set F)) → LinearIndepOn F (MulAction.toFun G F) s := by
classical
have : IsEmpty ((∅ : Finset F) : Set F) := by simp
refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
rw [coe_insert] at hs ⊢
rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F
by
replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
intro i his g
refine
eq_of_sub_eq_zero
(linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩ (mem_attach _ _) : _)
refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
ext g'; dsimp only
conv_lhs =>
rw [sum_apply]
congr
· skip
· ext
rw [Pi.smul_apply, sub_smul, smul_eq_mul]
rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
conv_lhs =>
congr
· skip
· ext x
rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
change
(∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'
rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ← sum_apply _ _ fun y => l y • toFun G F y]
rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
