smul_inv'' — Mathlib

English

If M acts on a division ring F by a semiring action, then action commutes with inversion: for x ∈ M and m ∈ F, x • m⁻¹ = (x • m)⁻¹.

Русский

Если M действует на делимой кольце F через действие умножения, то действие сохраняет обратное: x • m⁻¹ = (x • m)⁻¹.

LaTeX

$$$\\forall x:\\, M,\\; \\forall m:\\, F:\\; x \\cdot m^{-1} = (x \\cdot m)^{-1}$$$

Lean4

/-- 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) _

Похожие утверждения