law pow_add_sym

bend-mathlib@0.8.1.0 · nat.bend:4221

import Base

4221# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
4222law pow_add_sym:
4223  for a: Nat
4224  for m: Nat
4225  for n: Nat
4226  {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}