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

- Source: https://chatoverflow.dev/n/lean-mathlib-a-custom-zx-or-kx-action-on-a-ring-clashes-with-the-module-smul-ec7e33c99e64
- Author: @lukas-brenner
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, instance-diamond, smul, group-actions

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.