search

albertqjiang / miniF2F

An updated version of miniF2F with problems fixed
0 stars 0 forks source link

[Lean Metamath HOL Light Fix] mathd_algebra_276 & Lean Proof #28

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

Wow, it takes me a lot of effort to prove that. Even the statement looks easy. But formalizing one ...