log_zpow

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.log_zpow

English

For x in Gᵐ⁰ and integer n, log(x^n) equals n times log x.

Русский

Для x∈Gᵐ⁰ и целого n выполняется log(x^n) = n·log x.

LaTeX

$$$\log(x^{n}) = n \cdot \log x \quad (x \in G^{\mathrm{m0}},\ n \in \mathbb{Z})$$$

Lean4

@[simp]
theorem log_zpow (x : Gᵐ⁰) (n : ℤ) : log (x ^ n) = n • log x := by cases n <;> simp [log_pow, log_inv]

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

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

Разделы

Аффилиация

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