Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 11:19 4bfae3d8

View on Github →

feat(set_theory/game/pgame): remove nolint (#13680) We remove @[nolint has_inhabited_instance] from left_moves and right_moves by providing the appropriate instances for star.

Estimated changes