English
There exists an element c in F such that for every root α' of f.map ϕ in E and every root β' of g.map ϕ in E, the value -(α'−α)/(β'−β) is not in the image of ϕ, i.e., not equal to ϕ(c).
Русский
Существуют элементы c∈F такие, что для любых корней α' и β' полиномов f и g после отображения ϕ, выражение -(α'−α)/(β'−β) не лежит в образе ϕ.
LaTeX
$$$\exists c\in F,\ \forall α'\in (f.map\,\varphi).roots,\ \forall β'\in (g.map\,\varphi).roots,\ -(α'-α)/(β'-β)\neq \varphi c$$$
Lean4
theorem primitive_element_inf_aux_exists_c (f g : F[X]) :
∃ c : F, ∀ α' ∈ (f.map ϕ).roots, ∀ β' ∈ (g.map ϕ).roots, -(α' - α) / (β' - β) ≠ ϕ c := by
classical
let sf := (f.map ϕ).roots
let sg := (g.map ϕ).roots
classical
let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map] at hc
push_neg at hc
exact ⟨c, hc⟩
