law pow_add

bend-mathlib@0.8.1.0 · nat.bend:1232

import Base

1232# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1233law pow_add:
1234  for a: Nat
1235  for m: Nat
1236  for n: Nat
1237  {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}