Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 00:36 983cb905

View on Github →

feat(archive/imo): formalize 1987Q1 (#4731)

Estimated changes

Created archive/imo/imo1987_q1.lean

added theorem imo_1987_q1.card_fixed_points

added def imo_1987_q1.fiber

added def imo_1987_q1.fixed_points_equiv'

added def imo_1987_q1.fixed_points_equiv

added theorem imo_1987_q1.main

added theorem imo_1987_q1.main_fintype

added theorem imo_1987_q1.main₀

added theorem imo_1987_q1.mem_fiber

added def imo_1987_q1.p