mkRat_pow

Mathlib.Algebra.Ring.Rat

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

← MathLib Explorer

English

If a rational q is formed as mkRat num den, then q^n = mkRat (num^n) (den^n).

Русский

Если рацион q задан как mkRat num den, то q^n = mkRat (num^n) (den^n).

LaTeX

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

Lean4

@[simp]
theorem mkRat_pow (num den : ℕ) (n : ℕ) : mkRat num den ^ n = mkRat (num ^ n) (den ^ n) := by
  rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]

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

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

Разделы

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

Аффилиация

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