Commit 2024-06-29 08:10 99d09fff

View on Github →

feat(Data/Nat/Defs): pow_eq_self_iff (#14183) For a > 1, a ^ b = a iff b = 1. Lemma needed by #14049.

Estimated changes

added theorem Nat.pow_eq_self_iff