a_one_pow

Mathlib.GroupTheory.SpecificGroups.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionGroup.a_one_pow

← MathLib Explorer

English

For all k, (a_1)^k = a_k.

Русский

Для всех k, (a_1)^k = a_k.

LaTeX

$$$a_1^k = a_k$$$

Lean4

@[simp]
theorem a_one_pow (k : ℕ) : (a 1 : QuaternionGroup n) ^ k = a k := by
  induction k with
  | zero => rw [Nat.cast_zero]; rfl
  | succ k IH =>
    rw [pow_succ, IH, a_mul_a]
    congr 1
    norm_cast

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

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

Разделы

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

Аффилиация

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