Library Stdlib.ZArith.Zpow_def

From Stdlib Require Import BinInt Ring_theory.
#[local] Open Scope Z_scope.

Power functions over Z

Nota : this file is mostly deprecated. The definition of Z.pow and its usual properties are now provided by module BinInt.Z.

#[deprecated(since="Stdlib 9.1", note="Use setoid_ring.ZArithRing.Zpower_theory")]
Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.