induction_on_adjoin_fg — Mathlib

English

Let P be a property of intermediate fields. If P holds for ⊥ and if whenever K is a field and x ∈ E, P(K) implies P(K⟮x⟯.restrictScalars F) for all x, then P(K) holds for every FG intermediate field K.

Русский

Пусть P — свойство подполь. Если P верно для ⊥ и если для любого K и любого x ∈ E при условии P(K) следует P(K⟮x⟯.restrictScalars F) для всех x, тогда P(K) верно и для каждого FG-подполе K.

LaTeX

$$$\forall K (h : K.FG), P(K)$ по условию индукции$$

Lean4

theorem induction_on_adjoin_fg (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F)) (K : IntermediateField F E)
    (hK : K.FG) : P K := by
  obtain ⟨S, rfl⟩ := hK
  exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

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