isCyclotomicExtension_eq — Mathlib

English

For intermediate fields F1,F2 with IsCyclotomicExtension S K (F_i), we have F1 = F2.

Русский

Для промежуточных полей F1, F2 с IsCyclotomicExtension S K (F_i) имеем F1 = F2.

LaTeX

$$$\\text{IsCyclotomicExtension}(S,K,F_1) \\land \\text{IsCyclotomicExtension}(S,K,F_2) \\Rightarrow F_1 = F_2$$$

Lean4

theorem isCyclotomicExtension_eq (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension S K F₁]
    [h₂ : IsCyclotomicExtension S K F₂] : F₁ = F₂ :=
  toSubalgebra_inj.mp <| _root_.IsCyclotomicExtension.eq S F₁.toSubalgebra F₂.toSubalgebra

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