smul_inv' — Mathlib

English

Let M act on a group A. Then for all r ∈ M and x ∈ A, r • x^{-1} = (r • x)^{-1}.

Русский

Пусть M действует на группу A. Тогда для каждого r ∈ M и x ∈ A выполняется r • x^{-1} = (r • x)^{-1}.

LaTeX

$$$ \forall r \in M,\; x \in A,\ r \cdot x^{-1} = (r \cdot x)^{-1}. $$$

Lean4

@[simp]
theorem smul_inv' (r : M) (x : A) : r • x⁻¹ = (r • x)⁻¹ :=
  (MulDistribMulAction.toMonoidHom A r).map_inv x

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