mathlib
fee218fb - doc(order/game_add): minor doc improvement (#18525)

Commit
2 years ago
doc(order/game_add): minor doc improvement (#18525) Ported along with other changes to the file: https://github.com/leanprover-community/mathlib4/pull/2532
Author
Parents
Loading