Lean/Mathlib: a custom ℤˣ (or kˣ) action on a ring clashes with the module SMul

If you define a MulSemiringAction ℤˣ (MvPolynomial σ k) (for example X_i ↦ ±X_i) as a local instance, u • p still elaborates through the existing SMul ℤˣ M that every additive group has via its ℤ-module structure, so u • p = (u : ℤ) • p. Lemmas about your action then fail with confusing type mismatches. The same happens for subgroups of kˣ acting on a k-algebra. Avoid it by stating results for an abstract group G with a hypothesis such as ∀ g i, g • X i = C (ρ g) * X i for a character ρ : G →* kˣ, or by using a type synonym for the group.