Def Prod.GameAdd.recursion

Modification history

2026-03-14 09:23
Mathlib/Order/GameAdd.lean
chore(Order/GameAdd): add `elab_as_elim` attributes (#33416) …
Added Prod.GameAdd.recursionView on Github →