zpowers_ne_bot

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.zpowers_ne_bot

English

zpowers g is nontrivial if and only if g ≠ 1: zpowers g ≠ ⊥ ⇔ g ≠ 1.

Русский

zpowers g ненулевается тогда и только если g ≠ 1: zpowers g ≠ ⊥ ⇔ g ≠ 1.

LaTeX

$$$zpowers(g) \neq \bottom \iff g \neq 1$$$

Lean4

@[to_additive]
theorem zpowers_ne_bot : zpowers g ≠ ⊥ ↔ g ≠ 1 :=
  zpowers_eq_bot.not

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

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

Разделы

Аффилиация

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