divInt_pow

Mathlib.Algebra.Ring.Rat

URI: https://scilib.ai/kg/mathlib#Rat.divInt_pow

English

For num ∈ ℕ, den ∈ ℤ, and n ∈ ℕ, (num/den)^n = num^n / den^n.

Русский

Для num ∈ ℕ, den ∈ ℤ и n ∈ ℕ: (num/den)^n = num^n / den^n.

LaTeX

$$$\left(\frac{num}{den}\right)^n = \frac{num^n}{den^n}$$$

Lean4

@[simp]
theorem divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) : (num /. den) ^ n = num ^ n /. den ^ n := by
  simp [divInt_eq_div, div_pow]

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

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

Разделы

Аффилиация

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