law mul_pow

bend-mathlib@0.8.1.0 · nat.bend:2199

import Base

2199# A power of a product is the product of the powers: (a * b)^n = a^n * b^n.
2200law mul_pow:
2201  for +a: Nat
2202  for +b: Nat
2203  for n: Nat
2204  {Nat.pow(Nat.mul(a, b), n) == Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) : Nat}