rpow_add — Mathlib

English

If a is a unit, then a^(x+y) = a^x a^y.

Русский

Если a - единица модуля, тогда a^(x+y) = a^x a^y.

LaTeX

$$IsUnit a ⇒ a^{x+y} = a^x a^y$$

Lean4

theorem rpow_add {a : A} {x y : ℝ} (ha : IsUnit a) : a ^ (x + y) = a ^ x * a ^ y :=
  by
  have ha' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
  simp only [rpow_def]
  rw [← cfc_mul _ _ a]
  refine cfc_congr ?_
  intro z hz
  have : z ≠ 0 := by aesop
  simp [NNReal.rpow_add this _ _]

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