Mathlib.Algebra.Ring.Action.Field

[MulSemiringAction M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹

Full source

/-- Note that `smul_inv'` refers to the group case, and `smul_inv` has an additional inverse
on `x`. -/
@[simp]
theorem smul_inv'' [MulSemiringAction M F] (x : M) (m : F) : x • m⁻¹ = (x • m)⁻¹ :=
  map_inv₀ (MulSemiringAction.toRingHom M F x) _

Inverse Preservation under Multiplicative Semiring Action: $x \cdot m^{-1} = (x \cdot m)^{-1}$

Informal description

Let $M$ be a monoid acting multiplicatively on a division ring $F$ (i.e., $M$ has a multiplicative semiring action on $F$). Then for any $x \in M$ and any nonzero $m \in F$, the action of $x$ on the inverse of $m$ equals the inverse of the action of $x$ on $m$, i.e., $x \cdot m^{-1} = (x \cdot m)^{-1}$.