law mul_pow_sym

bend-mathlib@0.8.1.0 · nat.bend:4501

import Base

4501# A power of a product is the product of the powers: (a * b)^n = a^n * b^n, reversed to rewrite toward the simple side.
4502law mul_pow_sym:
4503  for +a: Nat
4504  for +b: Nat
4505  for n: Nat
4506  {Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) == Nat.pow(Nat.mul(a, b), n) : Nat}