mk_pow

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Localization.mk_pow

← MathLib Explorer

English

Powers commute with mk: mk a b)^n = mk(a^n, b^n).

Русский

Степени сохраняются под mk: mk a b^n = mk(a^n, b^n).

LaTeX

$$$ mk a b ^ n = mk (a^n) (b^n) $$$

Lean4

@[to_additive]
theorem mk_pow (n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n) := by
  induction n <;> simp [pow_succ, *, ← mk_mul, ← mk_one]

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

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

Разделы

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

Аффилиация

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