pow_eq_divInt — Mathlib

English

Raising a rational to a natural power equals numerator^n divided by denominator^n.

Русский

Возведение рационального числа в степень n равно числителю в степени n и знаменателю в той же степени.

LaTeX

$$$ \forall q \in \mathbb{Q}, \forall n \in \mathbb{N}, q^n = q.num^n /. q.den^n $$$

Lean4

theorem pow_eq_divInt (q : ℚ) (n : ℕ) : q ^ n = q.num ^ n /. q.den ^ n := by rw [pow_def, mk_eq_divInt, Int.natCast_pow]

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