mk_pow

Mathlib.Algebra.GroupWithZero.Associated

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

English

mk preserves powers: mk(a^n) = (mk(a))^n for any a ∈ M and n ∈ ℕ.

Русский

mk сохраняет степени: mk(a^n) = (mk(a))^n для любого a ∈ M и n ∈ ℕ.

LaTeX

$$$ \operatorname{mk}(a^{n}) = (\operatorname{mk}(a))^{n} \quad (a \in M, n \in \mathbb{N}) $$$

Lean4

theorem mk_pow (a : M) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n := by
  induction n <;> simp [*, pow_succ, Associates.mk_mul_mk.symm]

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

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

Разделы

Аффилиация

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