Stream: general

Topic: is this true without decidable

Johan Commelin (Sep 07 2018 at 13:11):

example (R : Type) [ring R] (i j : ℕ) (hnat : i ≠ j)
(hR : ((i : R) + 1) = ((j : R) + 1)) :
((1 : R) = (0 : R)) := sorry


Johan Commelin (Sep 07 2018 at 13:13):

If it is true, what is the one-line proof?
If it is not true, what is the one-line proof assuming [decidable_eq R]?

Johan Commelin (Sep 07 2018 at 13:15):

Never mind. This is completely false.

Johan Commelin (Sep 07 2018 at 13:16):

/me needs to relearn modular arithmetic

Johan Commelin (Sep 07 2018 at 13:18):

I thought this was my goal state. But it's not. i and j are coerced somewhere else. But I don't know where.

Johan Commelin (Sep 07 2018 at 13:18):

/me needs to look at the pp.all true variant of the goal state.

Last updated: May 08 2021 at 18:17 UTC