Function vstd::arithmetic::power::lemma_pow_distributes

pub broadcast proof fn lemma_pow_distributes(a: int, b: int, e: nat)

Expand description

ensures

#[trigger] pow(a * b, e) == pow(a, e) * pow(b, e),

Proof that a * b to the power of e is equal to the product of a to the power of e and b to the power of e

Function vstd::arithmetic::power::lemma_pow_distributesCopy item path