mathlib

039543c2 - refactor(set_theory/game/pgame): Simpler definition for `star` (#13869)

refactor(set_theory/game/pgame): Simpler definition for `star` (#13869) This new definition gives marginally easier proofs for the basic lemmas, and avoids use of the quite incomplete `of_lists` API.