Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.modeq.pow_card_sub_one_eq_one

Modification history

2021-12-13 09:36

src/field_theory/finite/basic.lean

feat(archive/imo): IMO 2005 problem 4 (modular arithmetic) (#10746)

Added int.modeq.pow_card_sub_one_eq_one View on Github →