nnrpow_nnrpow — Mathlib

English

For suitable A, (a^x)^y = a^(x*y) holds when x,y ≥ 0.

Русский

При подходящем A выполняется (a^x)^y = a^(x*y) при x,y ≥ 0.

LaTeX

$$(a^x)^y = a^(x*y)$$

Lean4

@[simp]
theorem nnrpow_nnrpow {a : A} {x y : ℝ≥0} : (a ^ x) ^ y = a ^ (x * y) :=
  by
  by_cases ha : 0 ≤ a
  case pos =>
    obtain (rfl | hx) := eq_zero_or_pos x <;> obtain (rfl | hy) := eq_zero_or_pos y
    all_goals try simp
    simp only [nnrpow_def]
    rw [← cfcₙ_comp _ _ a]
    congr! 2 with u
    ext
    simp [Real.rpow_mul]
  case neg => simp [nnrpow_def, cfcₙ_apply_of_not_predicate a ha]

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