mul_rpow — Mathlib

English

If x ≥ 0 and y ≥ 0, then (xy)^z = x^z y^z.

Русский

Если x ≥ 0 и y ≥ 0, тогда (xy)^z = x^z y^z.

LaTeX

$$$\\\\forall x \\\\ge 0, \\\\forall y \\\\ge 0, \\\\forall z: \ (xy)^z = x^z y^z.$$$

Lean4

theorem mul_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) : (x * y) ^ z = x ^ z * y ^ z :=
  by
  iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all
  · rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]
  all_goals positivity

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