[Merged by Bors] - chore(Algebra/TrivSqZeroExt): use open scoped RightActions

[eric-wieser]

One lemma statement has changed (up to associativity).

This is one of the more compelling justifications for #8909.

---

[j-loreaux]

This is indeed much nicer. I went through the file and saw a few places where I would prefer to change • to •> to aid the eye. I'm only interested in it in places where there is an op smul. Personally, I would like to prefer that as the default style (i.e., if a SMul Rᵐᵒᵖ M instance is in context, we write •> instead of •).

Because GitHub doesn't allow me to easily reference things not in the diff, I'll just list the line numbers: 526, 578, 624, 636, 646, 769.

[eric-wieser]

Because GitHub doesn't allow me to easily reference things not in the diff, I'll just list the line numbers:

1. mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 526 in a0ebb82

   show x.1 • (0 : M) + (1 : Rᵐᵒᵖ) • x.2 = x.2 by rw [smul_zero, zero_add, one_smul] }

   Slightly awkward because I have to then use op_one in the proof before I can use one_smul

2. mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 578 in a0ebb82

   show x.1 • (0 : M) + (0 : Rᵐᵒᵖ) • x.2 = 0 by rw [smul_zero, zero_add, zero_smul]

   Same, but for 0

3. mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 624 in a0ebb82

   (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd := by

   mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 636 in a0ebb82

   refine' (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) _).trans _

   In this case the point of the lemma is that the two actions are in this case the same; but maybe that's not so good an argument.

4. mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 646 in a0ebb82

   [IsCentralScalar R M] (x : tsze R M) (n : ℕ) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd :=

   I think the argument above applies more strongly here; if you have IsCentralScalar you never need to make the distinction

5. mathlib4/Mathlib/Algebra/TrivSqZeroExt.lean

   Line 769 in a0ebb82

   show r • x.snd = algebraMap S R r •> x.snd + (0 : M) <• x.fst by

   This is an action by S not R, which has no right action clearly I should change the variable name

[eric-wieser]

(i.e., if a SMul Rᵐᵒᵖ M instance is in context, we write •> instead of •).

It would be neat if we could teach the pretty-printer this rule.

[eric-wieser]

I've addressed 1 and 2 above, and made 5 moot by renaming. I've solved my objection to 3 by adding a second lemma stated with right actions, and I claim 4 needs no change.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style