mathlib
684587b0 - feat(set_theory/game/pgame): `add_lf_add_of_lf_of_le` (#14150)

Commit
3 years ago
feat(set_theory/game/pgame): `add_lf_add_of_lf_of_le` (#14150) This generalizes the previously existing `add_lf_add` on `numeric` games.
Author
Parents
Loading