repr_unop_eq_mulOpposite_repr

Mathlib.LinearAlgebra.Basis.MulOpposite

URI: https://scilib.ai/kg/mathlib#Module.Basis.repr_unop_eq_mulOpposite_repr

English

For x in H, the representation satisfies b.repr(unop x) = b.mulOpposite.repr(x).

Русский

Для x в H выполняется b.repr(unop x) = b.mulOpposite.repr(x).

LaTeX

$$b.repr(\mathrm{unop}(x)) = b.mulOpposite.repr(x)$$

Lean4

@[simp]
theorem repr_unop_eq_mulOpposite_repr (b : Basis ι R H) (x : Hᵐᵒᵖ) : b.repr (unop x) = b.mulOpposite.repr x :=
  rfl

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

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

Разделы

Аффилиация

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