Theorems · Theorem · number theory

IntermediateField.isCyclotomicExtension_eq

∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension S K ↥F₁] [h₂ : IsCyclotomicExtension S K ↥F₂], F₁ = F₂

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsCyclotomicExtensionIsCyclotomicExtension