complex-number-game icon indicating copy to clipboard operation
complex-number-game copied to clipboard

Published 20 hours ago • verified publisher icon ImperialCollegeLondon

Update to use Lean 3.48 & updated mathlib

Open arienmalec opened this issue 2 years ago • 0 comments

Updated Complex Number Game to use latest Lean 3 and mathlib. The "all in one" proof for comm_ring broke (presumably because the structure is more complicated in updated mathlib, so this PR includes the explicit proofs needed by comm_ring.

arienmalec avatar Nov 12 '22 00:11 arienmalec