Commit 2023-09-09 20:21 a14fcecb

View on Github →

feat: self_lt_pow (#7058)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Order.lean

added theorem self_lt_pow

Modified Mathlib/NumberTheory/FermatPsp.lean