splits_cyclotomic — Mathlib

English

If IsCyclotomicExtension S K L, then cyclotomic n K splits over L provided n ∈ S.

Русский

Если IsCyclotomicExtension S K L, то cyclotomic n K распадается в L при условии n ∈ S.

LaTeX

$$[IsCyclotomicExtension S K L] (n ∈ S) ⇒ Splits (algebraMap K L) (cyclotomic n K)$$

Lean4

/-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S`. -/
theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) : Splits (algebraMap K L) (cyclotomic n K) :=
  by
  refine splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero (NeZero.pos _) _) (splits_X_pow_sub_one K L hS) ?_
  use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K
  rw [(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl, RingHom.map_one]

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