Theorems · Theorem · field theory

IntermediateField.ext

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {S T : IntermediateField K L}, (∀ (x : L), x ∈ S ↔ x ∈ T) → S = T

Two intermediate fields are equal if they have the same elements.

Defined in

Mathlib.FieldTheory.IntermediateField.Basic

Cited by

17 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra