mkOfPowEq

Mathlib.RingTheory.RootsOfUnity.Basic

URI: https://scilib.ai/kg/mathlib#rootsOfUnity.mkOfPowEq

← MathLib Explorer

English

The coercion of mkOfPowEq ζ h equals ζ.

Русский

Укрощение mkOfPowEq ζ h равно ζ.

LaTeX

$$$\text{coe\_mkOfPowEq }(ζ,h) = ζ$$$

Lean4

/-- Make an element of `rootsOfUnity` from a member of the base ring, and a proof that it has
a positive power equal to one. -/
@[simps! coe_val]
def mkOfPowEq (ζ : M) {n : ℕ} [NeZero n] (h : ζ ^ n = 1) : rootsOfUnity n M :=
  ⟨Units.ofPowEqOne ζ n h <| NeZero.ne n, Units.pow_ofPowEqOne _ _⟩

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

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

Разделы

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

Аффилиация

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