of_comp — Mathlib

English

If T is EssFiniteType over R, then S is EssFiniteType over T (transitivity along the tower).

Русский

Если T имеет EssFiniteType над R, то S имеет EssFiniteType над T (третья вершина башни).

LaTeX

$$EssFiniteType R T ⇒ EssFiniteType S T$$

Lean4

theorem of_comp [h : EssFiniteType R T] : EssFiniteType S T :=
  by
  rw [essFiniteType_iff] at h ⊢
  classical
  obtain ⟨σ, hσ⟩ := h
  use σ
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := hσ x
  simp_rw [← Algebra.adjoin_adjoin_of_tower R (S := S) (σ : Set T)]
  exact ⟨y, Algebra.subset_adjoin hy₁, hy₂, Algebra.subset_adjoin hy₃⟩

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