Group action on fields

@[simp]

theorem smul_inv'' {M : Type u_1} [Monoid M] {F : Type u_2} [DivisionRing F] [MulSemiringAction M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹

Note that smul_inv' refers to the group case, and smul_inv has an additional inverse on x.