Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 10fb7f91

View on Github →

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

Estimated changes

Created archive/imo/imo2005_q4.lean

added def a

added theorem find_specified_factor

Modified src/field_theory/finite/basic.lean

added theorem int.modeq.pow_card_sub_one_eq_one