math2001 icon indicating copy to clipboard operation
math2001 copied to clipboard

possible copy/paste errors in 07_Euclidean_Algorithm.lean

Open ketilwright opened this issue 1 year ago • 0 comments

There is a theorem gcd_dvd starting about line 60 of this file. It's not clear if the reader should resolve the 8 sorries or not. I think not since gcd_dvd_right & left come next.

In any case: Following the split_ifs with h1 h2 . . ., and preceding each "sorry", is the comment "prove that gcd a b | b" (or | a).

In no case does the comment reflect the current goal. For example, the first goal is gcd b (fmod a b) ∣ b, the next is gcd b (fmod a b) ∣ a, etc,

ketilwright avatar Jul 24 '24 22:07 ketilwright