difference of squares of commuting elements

Stream: Is there code for X?

[Eric Wieser]

Does something like this exist anywhere?

lemma commute.mul_self_sub_mul_self_eq {R} [ring R] {a b : R}(h : commute a b) :
  a * a - b * b = (a + b) * (a - b) :=
begin
  rw [add_mul, mul_sub, mul_sub, h.eq],
  abel,
end

lemma commute.mul_self_sub_mul_self_eq' {R} [ring R] {a b : R} (h : commute a b) :
  a * a - b * b = (a - b) * (a + b) :=
begin
  rw [mul_add, sub_mul, sub_mul, h.eq],
  abel,
end

[Eric Wieser]

docs#mul_self_sub_mul_self exists but requires commutativity

[Eric Wieser]

#12366

[Johan Commelin]

Does it make sense to flip these, and call them commute.add_mul_sub_eq and commute.sub_mul_add_eq?

[Eric Wieser]

I was certainly tempted to do that

[Eric Wieser]

Although arguably add_mul_sub is more ambiguous than mul_self_sub_mul_self

[Eric Wieser]

I figured that whoever added the lemma in the first place probably thought of that name too, and since I didn't feel that strongly I'd just leave it unchanged.