English
If γ lies in the field generated by α and β, and P holds for α and β, then P holds for γ.
Русский
Если γ принадлежит полю, получаемому порождением α и β, и P выполняется для α и β, то P выполняется для γ.
LaTeX
$$$$\gamma \in F\langle \alpha, \beta \rangle \Rightarrow P(\alpha) \wedge P(\beta) \Rightarrow P(\gamma)$$$$
Lean4
theorem induction (P : solvableByRad F E → Prop) (base : ∀ α : F, P (algebraMap F (solvableByRad F E) α))
(add : ∀ α β : solvableByRad F E, P α → P β → P (α + β)) (neg : ∀ α : solvableByRad F E, P α → P (-α))
(mul : ∀ α β : solvableByRad F E, P α → P β → P (α * β)) (inv : ∀ α : solvableByRad F E, P α → P α⁻¹)
(rad : ∀ α : solvableByRad F E, ∀ n : ℕ, n ≠ 0 → P (α ^ n) → P α) (α : solvableByRad F E) : P α :=
by
revert α
suffices ∀ α : E, IsSolvableByRad F α → ∃ β : solvableByRad F E, ↑β = α ∧ P β
by
intro α
obtain ⟨α₀, hα₀, Pα⟩ := this α (Subtype.mem α)
convert Pα
exact Subtype.ext hα₀.symm
apply IsSolvableByRad.rec
· exact fun α => ⟨algebraMap F (solvableByRad F E) α, rfl, base α⟩
· intro α β _ _ Pα Pβ
obtain ⟨⟨α₀, hα₀, Pα⟩, β₀, hβ₀, Pβ⟩ := Pα, Pβ
exact ⟨α₀ + β₀, by rw [← hα₀, ← hβ₀]; rfl, add α₀ β₀ Pα Pβ⟩
· intro α _ Pα
obtain ⟨α₀, hα₀, Pα⟩ := Pα
exact ⟨-α₀, by rw [← hα₀]; rfl, neg α₀ Pα⟩
· intro α β _ _ Pα Pβ
obtain ⟨⟨α₀, hα₀, Pα⟩, β₀, hβ₀, Pβ⟩ := Pα, Pβ
exact ⟨α₀ * β₀, by rw [← hα₀, ← hβ₀]; rfl, mul α₀ β₀ Pα Pβ⟩
· intro α _ Pα
obtain ⟨α₀, hα₀, Pα⟩ := Pα
exact ⟨α₀⁻¹, by rw [← hα₀]; rfl, inv α₀ Pα⟩
· intro α n hn hα Pα
obtain ⟨α₀, hα₀, Pα⟩ := Pα
refine ⟨⟨α, IsSolvableByRad.rad α n hn hα⟩, rfl, rad _ n hn ?_⟩
convert Pα
exact Subtype.ext (Eq.trans ((solvableByRad F E).coe_pow _ n) hα₀.symm)
