pow

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.pow

English

If a is a unit, then a^n is a unit for every natural n.

Русский

Если a — единица, то a^n — единица для любого натурального n.

LaTeX

$$IsUnit(a) \rightarrow IsUnit(a^n)$$

Lean4

@[to_additive]
theorem pow (n : ℕ) : IsUnit a → IsUnit (a ^ n) := by rintro ⟨u, rfl⟩; exact ⟨u ^ n, rfl⟩

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

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

Разделы

Аффилиация

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