Commit 2024-10-22 12:13 9e395964

View on Github →

chore(Archive): use newly introduced finset notation (#18052)

Estimated changes

Modified Archive/Imo/Imo1994Q1.lean

modified theorem imo1994_q1

Modified Archive/Imo/Imo2021Q1.lean

Modified Archive/Sensitivity.lean

Modified Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

Modified Archive/Wiedijk100Theorems/Partition.lean

modified theorem Theorems100.partition_theorem

Modified Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

modified def Theorems100.P

modified def Theorems100.U

modified theorem Theorems100.card_le_mul_sum

modified theorem Theorems100.card_le_two_pow

modified theorem Theorems100.card_le_two_pow_mul_sqrt