of_tower_top_of_subalgebra_le — Mathlib

English

If A ≤ B are subalgebras of S and x is transcendental over B, then x is transcendental over A.

Русский

Если A ≤ B — подалгебры S, и x трансцендентен над B, то x трансцендентен над A.

LaTeX

$$$A \le B \Rightarrow (\mathrm{Transcendental}\ B\ x \Rightarrow \mathrm{Transcendental}\ A\ x)$$$

Lean4

/-- A special case of `Transcendental.restrictScalars`. This is extracted as a theorem
  because in some cases `Transcendental.restrictScalars` will just runs out of memory. -/
theorem of_tower_top_of_subalgebra_le {A B : Subalgebra R S} (hle : A ≤ B) {x : S} (h : Transcendental B x) :
    Transcendental A x := fun H ↦ h (H.tower_top_of_subalgebra_le hle)

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