Commit 2022-11-20 09:55 9a1d2823

View on Github →

feat: port Order.GameAdd (#645) mathlib SHA: fd47bdf09e90f553519c712378e651975fe8c829

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Init/Align.lean

Created Mathlib/Order/GameAdd.lean

added theorem Acc.prod_gameAdd

added inductive Prod.GameAdd

added theorem Prod.gameAdd_le_lex

added theorem Prod.rprod_le_transGen_gameAdd

added theorem WellFounded.prod_gameAdd