algebraicClosure — Mathlib

English

If a ∈ E is transcendental over F, then its image in algebraicClosure F E is transcendental over F.

Русский

Если элемент a ∈ E трансцендентен над F, то его образ в algebraicClosure F E также трансцендентен над F.

LaTeX

$$$ \\text{If } a \\in E \\text{ and } a \\text{ is transcendental over }F, \\ \\text{then } a \\text{ is transcendental over }F \\text{ in } \\operatorname{algebraicClosure}_F(E)$$$

Lean4

protected theorem algebraicClosure {a : E} (ha : Transcendental F a) : Transcendental (algebraicClosure F E) a :=
  ha.extendScalars _

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