of_tower_top — 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

/-- If `x` is transcendental over `L`, then `x` is transcendental over `K` when
  `L` is an extension of `K` -/
theorem of_tower_top {x : A} (h : Transcendental L x) : Transcendental K x := fun H ↦ h (H.tower_top L)

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