induction_on_adjoin — Mathlib

English

The finrank of the compositum E1 ⊔ E2 over K is at most the product of finranks: finrank_K( E1 ⊔ E2 ) ≤ finrank_K E1 × finrank_K E2.

Русский

Размерность по модулю finrank над K от композиции E1 ⊔ E2 не превосходит произведение размерностей: finrank_K( E1 ⊔ E2 ) ≤ finrank_K E1 · finrank_K E2.

LaTeX

$$finrank_K( E1 ⊔ E2 ) ≤ finrank_K E1 · finrank_K E2$$

Lean4

theorem induction_on_adjoin [FiniteDimensional F E] (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) : P K :=
  letI : IsNoetherian F E := IsNoetherian.iff_fg.2 inferInstance
  induction_on_adjoin_fg P base ih K K.fg_of_noetherian

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