law pow_mul

bend-mathlib@0.8.1.0 · nat.bend:2214

import Base

2214# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n.
2215law pow_mul:
2216  for a: Nat
2217  for m: Nat
2218  for n: Nat
2219  {Nat.pow(a, Nat.mul(m, n)) == Nat.pow(Nat.pow(a, m), n) : Nat}