Commit 2023-03-27 23:46 426aed39

View on Github →

feat: port changes to order/game_add (#2532) Simultaneously ports various PRs on this file. This also fixes a mis-ported alias in Mathlib/Order/RelIso/Basic.lean

Estimated changes

added theorem Acc.sym2_gameAdd
added theorem Prod.GameAdd.fix_eq
added theorem Prod.GameAdd.induction
added theorem Prod.GameAdd.to_sym2
added theorem Prod.gameAdd_iff
added theorem Prod.gameAdd_mk_iff
added theorem Prod.gameAdd_swap_swap
added theorem Sym2.GameAdd.fix_eq
added theorem Sym2.GameAdd.fst
added theorem Sym2.GameAdd.fst_snd
added theorem Sym2.GameAdd.induction
added theorem Sym2.GameAdd.snd
added theorem Sym2.GameAdd.snd_fst
added def Sym2.GameAdd
added theorem Sym2.gameAdd_iff
added theorem Sym2.gameAdd_mk'_iff