pow_eq_mkRat — Mathlib

English

Raising a rational to a natural power corresponds to raising numerator and denominator to that power and then forming mkRat.

Русский

Возведение рационального числа в натуральную степень соответствует возведению числителя и знаменателя в эту степень и построению mkRat.

LaTeX

$$$ \forall (q : \mathbb{Q}) (n : \mathbb{N}), q^n = mkRat (q.num^n) (q.den^n) $$$

Lean4

theorem pow_eq_mkRat (q : ℚ) (n : ℕ) : q ^ n = mkRat (q.num ^ n) (q.den ^ n) := by rw [pow_def, mk_eq_mkRat]

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