rootsOfUnity_one

Mathlib.RingTheory.RootsOfUnity.Basic

URI: https://scilib.ai/kg/mathlib#rootsOfUnity_one

← MathLib Explorer

English

The underlying value of the constructed root mkOfPowEq ζ h equals ζ.

Русский

Опорное значение сконструированного корня mkOfPowEq ζ h равно ζ.

LaTeX

$$$((\mathrm{rootsOfUnity.mkOfPowEq} \zeta h).val).val = \zeta$$$

Lean4

@[simp]
theorem rootsOfUnity_one (M : Type*) [CommMonoid M] : rootsOfUnity 1 M = ⊥ :=
  by
  ext1
  simp only [mem_rootsOfUnity, pow_one, Subgroup.mem_bot]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru