Commit 2025-06-07 16:11 cb99f5a5

View on Github →

chore: deprime induction in Archive and SetTheory (#25512) I have decided that depriming one folder (or part of a folder) at a time is the way to go.

Estimated changes

Modified Archive/Imo/Imo1977Q6.lean

Modified Archive/Imo/Imo2006Q5.lean

Modified Archive/Imo/Imo2013Q1.lean

Modified Archive/Imo/Imo2013Q5.lean

Modified Archive/Imo/Imo2019Q1.lean

Modified Archive/Imo/Imo2019Q4.lean

Modified Archive/Imo/Imo2024Q1.lean

Modified Archive/MiuLanguage/DecisionSuf.lean

Modified Archive/OxfordInvariants/Summer2021/Week3P1.lean

Modified Archive/Sensitivity.lean

modified theorem Sensitivity.f_matrix

Modified Archive/Wiedijk100Theorems/FriendshipGraphs.lean

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

Modified Mathlib/SetTheory/Descriptive/Tree.lean

Modified Mathlib/SetTheory/Game/Birthday.lean

Modified Mathlib/SetTheory/Game/Nim.lean

Modified Mathlib/SetTheory/Lists.lean

added def Lists'.recOfList

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Surreal/Basic.lean

Modified Mathlib/SetTheory/Surreal/Dyadic.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

Modified Mathlib/SetTheory/ZFC/Rank.lean