isCyclotomicExtension_le_of_dvd — Mathlib

English

If n1 divides n2, then the corresponding cyclotomic extensions satisfy C1 ≤ C2.

Русский

Если n1 делится на n2, то соответствующие циклотомические расширения удовлетворяют C1 ≤ C2.

LaTeX

$$$n_1 \\mid n_2 \\Rightarrow C_1 \\le C_2$$$

Lean4

theorem isCyclotomicExtension_le_of_dvd [NeZero n₂] (h : n₁ ∣ n₂) : F₁ ≤ F₂ := by
  exact toSubalgebra_le_toSubalgebra.mp <| IsCyclotomicExtension.le_of_dvd n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra h

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