zero

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

URI: https://scilib.ai/kg/mathlib#IsPrimitiveRoot.zero

English

In a nontrivial monoid with zero, the element 0 is a primitive root of order 0.

Русский

В ненулевом моноиде с нулём элемент 0 является примитивным корнем порядка 0.

LaTeX

$$$$\text{zero is a primitive root of order }0:\ IsPrimitiveRoot(0,0).$$$$

Lean4

theorem zero [Nontrivial M₀] : IsPrimitiveRoot (0 : M₀) 0 :=
  ⟨pow_zero 0, fun l hl ↦ by simpa [zero_pow_eq] using hl⟩

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

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

Разделы

Аффилиация

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