smul_smul_smul_comm

Stream: general

[Yaël Dillies]

Do you want such an abomination in mathlib?

import algebra.algebra.basic

lemma smul_smul_smul_comm {α β γ δ : Type*} [has_scalar α β] [has_scalar α γ] [has_scalar β δ]
  [has_scalar α δ] [has_scalar γ δ] [is_scalar_tower α β δ] [is_scalar_tower α γ δ]
  [smul_comm_class β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
  (a • b) • (c • d) = (a • c) • b • d :=
by { rw [smul_assoc, smul_assoc, smul_comm b], apply_instance }

[Thomas Browning]

Several times now, I've run into things sort of like this (e.g., (a+b)+(c+d)=(a+c)+(b+d)), and wished that mathlib had the lemma.

[Yaël Dillies]

docs#add_add_add_comm :wink: (I think I added that one?)

[Yaël Dillies]

Ah no, I don't remember which one I added then

[Johan Commelin]

It's time for a smaug tactic, which is like ring, but for smul. :stuck_out_tongue_wink:

[Bhavik Mehta]

Johan Commelin said:

It's time for a smaug tactic, which is like ring, but for smul. :stuck_out_tongue_wink:

Perhaps @Patrick Stevens might want to write this :stuck_out_tongue_closed_eyes:

[Patrick Stevens]

Hah, there's a blast from the past! (Bhavik and I interacted during the National Cipher Challenge a decade ago, where I had the username Smaug.)

[Johan Commelin]

You still have on github, don't you?

[Patrick Stevens]

Oh I do - I forgot its vestiges were still with me, so in fact no backstory is required

[Mario Carneiro]

I think we should certainly have this lemma where applicable. If I added it, it will probably have the name add_comm_four or something like it