eq_zero_of_add_eq_zero_right

Stream: std4

[Kevin Buzzard]

My instinct with docs#Nat.eq_zero_of_add_eq_zero_right (n + m = 0 → n = 0) would have been to call it Nat.eq_zero_of_add_right_eq_zero (i.e. move the word right). I'm threatening to call it this in NNG and hence cause confusion, but if I've misunderstood the naming convention can someone let me know ASAP? :-)

[Ruben Van de Velde]

I guess it's two variants of eq_zero_of_add_eq_zero, the left one and the right one

[Eric Wieser]

Is the intent to use the docs#add_right_injective meaning of right, or the docs#add_right_cancel meaning?

[Kevin Buzzard]

The intent was to use the docs#add_right_eq_self meaning, which is the lemma I'd just proved beforehand. The two conventions for location of right looked a bit weird to me when put next to each other.

[Joe Hendrix]

The left and right seem a bit confusing to me too here. It kind of feels like "n + m = 0 -> n = 0 /\ m = 0" would be easier to name (eq_zero_of_add_eq_zero or add_eq_zero_eq_zero) and then one could get separately get either equation out of the and separately.

[Kevin Buzzard]

Yeah but in my game the user is only going to prove one of these conclusions (not least because I didn't introduce and yet!) so I still need to name the weaker lemmas