isIntegral — Mathlib

English

An auxiliary induction step: from P(α^n) under certain conditions to P(α).

Русский

Вспомогательный шаг индукции: из P(α^n) при некоторых условиях следует P(α).

LaTeX

$$$$\text{Induction3: } \text{if } P(α^n) \text{ and } n \neq 0, \Rightarrow P(α).$$$$

Lean4

theorem isIntegral (α : solvableByRad F E) : IsIntegral F α :=
  by
  revert α
  apply solvableByRad.induction
  · exact fun _ => isIntegral_algebraMap
  · exact fun _ _ => IsIntegral.add
  · exact fun _ => IsIntegral.neg
  · exact fun _ _ => IsIntegral.mul
  · intro α hα
    exact IsIntegral.inv hα
  · intro α n hn hα
    obtain ⟨p, h1, h2⟩ := hα.isAlgebraic
    refine
      IsAlgebraic.isIntegral
        ⟨p.comp (X ^ n), ⟨fun h => h1 (leadingCoeff_eq_zero.mp ?_), by rw [aeval_comp, aeval_X_pow, h2]⟩⟩
    rwa [← leadingCoeff_eq_zero, leadingCoeff_comp, leadingCoeff_X_pow, one_pow, mul_one] at h
    rwa [natDegree_X_pow]

Похожие утверждения