mathlib

d217e1db - feat(set_theory/game/pgame): `sub_self_equiv` (#14272)