comp_id_id — Mathlib

English

Applying congruence with the identity map on the domain yields a bilinear form equal to the original form on the new domain, i.e., congr (refl) = refl.

Русский

Применение конгруэнции с тождественным отображением на области определений даёт форму, равную исходной форме в новой области; конгруэнция(тождество) = тождество.

LaTeX

$$$ congr (LinearEquiv.refl\, R\, M) = LinearEquiv.refl\, R\, (LinearMap.BilinForm\, R\, M) $$$

Lean4

@[simp high]
theorem comp_id_id (B : BilinForm R M) : B.comp LinearMap.id LinearMap.id = B :=
  by
  ext
  rfl

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