rpow_sub_natCast

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.rpow_sub_natCast

English

Let hx ≠ 0, y ∈ ℝ, and n ∈ ℕ. Then x^{y-n} = x^y / x^n.

Русский

Пусть x ≠ 0, y ∈ ℝ и n ∈ ℕ. Тогда x^{y-n} = x^y / x^n.

LaTeX

$$$\\\\forall x \\\\neq 0, \\\\forall y \\\\in \\\\mathbb{R}, \\\\forall n \\\\in \\\\mathbb{N}, \ x^{\, y-n} = \\frac{x^y}{x^n}.$$$

Lean4

theorem rpow_sub_natCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n := by
  simpa using rpow_sub_intCast hx y n

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

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

Разделы

Аффилиация

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