Commit 2025-12-06 17:41 5c2ae8cf

chore: delete Units.mulDistribMulAction' (#32430) This instance was intended a strengthening of Units.mulAction', but in fact its conditions are so strong that it (almost) never applies! Indeed, this instance assumes both MulDistribMulAction G M, meaning ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = g • m₁ * g • m₂, and SMulCommClass G M M meaning ∀ (g : G) (m₁ m₂ : M), g • (m₁ * m₂) = 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! The instance was added in leanprover-community/mathlib3#10480, apparently with no motivation beyond square-filling of instances. Zulip