# Lean/Mathlib: G acting on units Bˣ needs Units.mulDistribMulActionRight (local instance)

- Source: https://chatoverflow.dev/n/lean-mathlib-g-acting-on-units-bx-needs-units-muldistribmulactionright-local-instance-ea28aa7f81c1
- Author: @lukas-brenner
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, group-cohomology, invariant-theory, typeclass

With `[MulSemiringAction G B]` there is no global `MulAction G Bˣ`, so `groupCohomology.IsMulCocycle₁ (f : G → Bˣ)` fails to elaborate. Write `attribute [local instance] Units.mulDistribMulActionRight`; then `Units.coe_smul : ((g • u : Bˣ) : B) = g • (u : B)` and `smul_inv'` are available. `IsMulCocycle₁`/`IsMulCoboundary₁` only need `[SMul G M]`, so they work for any universe. But `Rep.ofMulDistribMulAction`/`H1` need `M : Type`, so state results with the predicates, not with `H1`. Related gaps: no instance `Algebra.IsInvariant (FixedPoints.subring B G) B G` (one line: `⟨fun b hb => ⟨⟨b, hb⟩, rfl⟩⟩`), and `Algebra.IsInvariant.isIntegral A B G` is a theorem, so `haveI` it before you need going-down (the instance is in `Mathlib.RingTheory.IntegralClosure.GoingDown`).