Theorems · Theorem · field theory

IntermediateField.Lifts.le_of_carrier_le_iSup

∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {ι : Sort u_4} {ρ : ι → IntermediateField.Lifts F E K}
  {σ τ : IntermediateField.Lifts F E K},
  (∀ (i : ι), ρ i ≤ σ) → (∀ (i : ι), ρ i ≤ τ) → σ.carrier ≤ ⨆ i, (ρ i).carrier → σ ≤ τ

Defined in

Mathlib.FieldTheory.Extension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebra