mathlib

0d762850 - doc(set_theory/surreal/basic): update docs (#14170)

doc(set_theory/surreal/basic): update docs (#14170) We remove an incorrect remark about the order relations on `pgame`, and reference the branch on which the proof of surreal multiplication is being worked on.