tensorRId_symm_apply

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

URI: https://scilib.ai/kg/mathlib#QuadraticForm.tensorRId_symm_apply

English

For Q1 and x in M1 ⊗ R, the base isometry tensorRId Q1 applied to x equals TensorProduct.rid on x.

Русский

Для Q1 и x в M1 ⊗ R изометрия tensorRId Q1 применяется к x как TensorProduct.rid x.

LaTeX

$$$tensorRId\, Q_1\, x = \\, TensorProduct.rid\, R\, M_1\, x$$$

Lean4

@[simp]
theorem tensorRId_symm_apply (Q₁ : QuadraticForm R M₁) (x : M₁) :
    (tensorRId Q₁).symm x = (TensorProduct.rid R M₁).symm x :=
  rfl

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

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

Разделы

Аффилиация

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