lean_workbook_plus_29816
Proveda) Let be the number of players and the number of minutes played by each player. Then since both sides is equal to the total number of minutes played. Since , . Since , . If each player has to play for minutes. It is possible with players. Label the players . We start with the players on the field. For each is substituted with (indices are considered modulo ) after minutes have been played. Then each player plays exactly minutes, so the minimum number of players required is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29816 (n k : ℕ) (h₀ : 0 < n ∧ 0 < k) (h₁ : k < 60) (h₂ : (n * k) = 90 * 11) : 18 ≤ n := by sorry
Source