feat: MulDistribMulAction M Nˣ instance (leanprover-community#32432)

From ClassFieldTheory

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/MulDistribMulAction.20instances)

Author: YaelDillies

Mathlib/Algebra/Group/Action/Units.lean

@@ -122,6 +122,36 @@ instance isScalarTower'_left [Group G] [Monoid M] [MulAction G M] [SMul M α] [S
 example [Monoid M] [Monoid N] [MulAction M N] [SMulCommClass M N N] [IsScalarTower M N N] :
     MulAction Mˣ Nˣ := Units.mulAction'
 
+section MulDistribMulAction
+variable {M N : Type*} [Monoid M] [Monoid N] [MulDistribMulAction M N]
+
+/-- Note this has different defeqs than `Units.mulAction'`, but doesn't create a diamond
+with it in non-degenerate situations. Indeed, to get a diamond on `MulDistribMulAction G Mˣ`,
+we would need both instances to fire. But `Units.mulAction'` assumes `SMulCommClass G M M`,
+i.e. `∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = m₁ * g • m₂`), while
+`Units.instMulDistribMulActionRight` assumes `MulDistribMulAction G M`,
+i.e. `∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂`.
+In particular, if `M` is cancellative, then we obtain `∀ (g : G) (m : M), g • m = m`,
+i.e. the action is trivial!
+
+This however does create a (propeq) diamond for `MulDistribMulAction (ConjAct Mˣ) Mˣ` with
+`ConjAct.unitsMulDistribMulAction` and `ConjAct.instMulDistribMulAction`. Indeed, if we go down
+one way then `u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * v⁻¹ * ofConjAct u⁻¹, _, _⟩`,
+while the other way is
+`u • v := ⟨ofConjAct u * v * ofConjAct u⁻¹, ofConjAct u * (v⁻¹ * ofConjAct u⁻¹), _, _⟩`. -/
+abbrev mulDistribMulActionRight : MulDistribMulAction M Nˣ where
+  smul m u := ⟨m • u, m • u⁻¹, by simp [← smul_mul', smul_one], by simp [← smul_mul', smul_one]⟩
+  one_smul u := Units.ext <| one_smul ..
+  mul_smul m₁ m₂ u := Units.ext <| mul_smul ..
+  smul_mul m₁ u₁ u₂ := Units.ext <| smul_mul' ..
+  smul_one m := Units.ext <| smul_one m
+
+attribute [local instance] mulDistribMulActionRight
+
+@[simp, norm_cast] lemma coe_smul (m : M) (u : Nˣ) : (m • u).val = m • u.val := rfl
+@[simp, norm_cast] lemma coe_inv_smul (m : M) (u : Nˣ) : (m • u)⁻¹.val = m • u⁻¹.val := rfl
+
+end MulDistribMulAction
 end Units
 
 @[to_additive]