of_card_le — Mathlib

English

If R is a domain and n ≤ card(rootsOfUnity n R), then HasEnoughRootsOfUnity R n.

Русский

Пусть R — домен и n ≤ card(rootsOfUnity n R); тогда HasEnoughRootsOfUnity R n.

LaTeX

$$HasEnoughRootsOfUnity.of_card_le: n ≤ card (rootsOfUnity n R) → HasEnoughRootsOfUnity R n$$

Lean4

theorem of_card_le {R : Type*} [CommRing R] [IsDomain R] {n : ℕ} [NeZero n] (h : n ≤ Fintype.card (rootsOfUnity n R)) :
    HasEnoughRootsOfUnity R n
    where
  prim := card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot.mp (le_antisymm (card_rootsOfUnity R n) h)
  cyc := rootsOfUnity.isCyclic R n

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