compRight_id

Mathlib.LinearAlgebra.BilinearForm.Hom

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.compRight_id

← MathLib Explorer

English

Reaffirmation that B.compRight id equals B in bilinear form context.

Русский

Повторное утверждение: B.compRight id = B в контексте билинейной формы.

LaTeX

$$$ B.compRight LinearMap.id = B $$$

Lean4

@[simp]
theorem compRight_id (B : BilinForm R M) : B.compRight LinearMap.id = B :=
  by
  ext
  rfl
    -- Shortcut for `comp_id_{left,right}` followed by `comp{Right,Left}_id`,
    -- Needs higher priority to be applied

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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