of_symm_sub — Mathlib

English

Under the same setup, the inverse embedding preserves subtraction: (of R).symm (x - y) = (of R).symm x - (of R).symm y.

Русский

В той же постановке обратное отображение сохраняет вычитание: (of R).symm (x − y) = (of R).symm x − (of R).symm y.

LaTeX

$$$((of\,R).symm (x - y)) = (of\,R).symm x - (of\,R).symm y$$$

Lean4

@[simp]
theorem of_symm_sub [AddCommGroup V] (x y : HahnModule Γ R V) : (of R).symm (x - y) = (of R).symm x - (of R).symm y :=
  rfl

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