isField_of_algebraic — Mathlib

English

In an algebraic extension L/K, any intermediate subalgebra is a field.

Русский

В алгебраическом расширении L/K любой промежуточной подалгеброй является полем.

LaTeX

$$$\\text{In an algebraic extension } L/K,\\text{ any intermediate subalgebra } A \\text{ is a field.}$$$

Lean4

/-- In an algebraic extension L/K, an intermediate subalgebra is a field. -/
@[stacks 0BID]
theorem isField_of_algebraic [Algebra.IsAlgebraic K L] : IsField A :=
  { show Nontrivial A by infer_instance, Subalgebra.toCommRing A with
    mul_inv_cancel := fun {a} ha =>
      ⟨⟨a⁻¹, A.inv_mem_of_algebraic (Algebra.IsAlgebraic.isAlgebraic (a : L))⟩,
        Subtype.ext (mul_inv_cancel₀ (mt (Subalgebra.coe_eq_zero _).mp ha))⟩ }

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