invOf_sym — Mathlib

English

If a is invertible in α, then sym(a)^{-1} = sym(a^{-1}) in the symmetrized algebra, matching the simplification symmetry.

Русский

Если a обратим в α, то в симметризованной алгебре выполняется sym(a)^{-1} = sym(a^{-1}).

LaTeX

$$$(\operatorname{sym} a)^{-1} = \operatorname{sym}(a^{-1})$$$

Lean4

@[simp]
theorem invOf_sym [Mul α] [AddMonoidWithOne α] [Invertible (2 : α)] (a : α) [Invertible a] : ⅟(sym a) = sym (⅟a) :=
  rfl

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