Theorem Prod.GameAdd.recursion_eq

Modification history

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