rootsOfUnity_le_of_dvd — Mathlib

English

A monoid homomorphism between units preserves roots of unity: map of rootsOfUnity under f is contained in rootsOfUnity in the target.

Русский

Гомоморфизм единиц сохраняет корни единства: образ подгруппы rootsOfUnity переходит в rootsOfUnity в целевом кольце.

LaTeX

$$$\text{map}_{f}(\mathrm{rootsOfUnity}(k,M)) \leq \mathrm{rootsOfUnity}(k,N)$$$

Lean4

theorem rootsOfUnity_le_of_dvd (h : k ∣ l) : rootsOfUnity k M ≤ rootsOfUnity l M :=
  by
  obtain ⟨d, rfl⟩ := h
  intro ζ h
  simp_all only [mem_rootsOfUnity, pow_mul, one_pow]

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