sym_inv

Mathlib.Algebra.Symmetrized

URI: https://scilib.ai/kg/mathlib#SymAlg.sym_inv

English

If α has an inversion, then sym(a)⁻¹ = (sym(a))⁻¹ = sym(a⁻¹).

Русский

Если у α есть обратимый элемент, то sym(a)⁻¹ = (sym(a))⁻¹ = sym(a⁻¹).

LaTeX

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

Lean4

@[simp, to_additive existing]
theorem sym_inv [Inv α] (a : α) : sym a⁻¹ = (sym a)⁻¹ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru