search

albertqjiang / miniF2F

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

[Metamath HOL Light Fix][Lean Proof] mathd_algebra_17 #30

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

This statement makes use of the fact that real.sqrt is truncated to 0 for negative input. We should be careful about the other versions.

@Wenda302 I also patched the Isabelle version here. Plz take a look if it's fine as I didn't check it with an Isabelle environment.

DyeKuu commented 2 years ago

Oh sorry didn't see your PR @Wenda302 , I'll revert the change for Isabelle here.