mulOpposite_repr_op

Mathlib.LinearAlgebra.Basis.MulOpposite

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

English

The opposite basis representation acts compatibly with op: b.mulOpposite.repr (op x) = b.repr x.

Русский

Представление противоположного базиса удовлетворяет: b.mulOpposite.repr (op x) = b.repr x.

LaTeX

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

Lean4

@[simp]
theorem mulOpposite_repr_op (b : Basis ι R H) (x : H) : b.mulOpposite.repr (op x) = b.repr x :=
  rfl

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

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

Разделы

Аффилиация

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