instInvertibleCoeEquivSym — Mathlib

English

If a is invertible in α, then its symmetrized version sym(a) is invertible in the symmetrized algebra, and its inverse is sym(a^{-1}).

Русский

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

LaTeX

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

Lean4

instance [Mul α] [AddMonoidWithOne α] [Invertible (2 : α)] (a : α) [Invertible a] : Invertible (sym a)
    where
  invOf := sym (⅟a)
  invOf_mul_self := by rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
  mul_invOf_self := by rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]

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