congr_congr

Mathlib.LinearAlgebra.BilinearForm.Hom

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

English

The congruence operation commutes with taking symmetries: congr e symm equals symm of congr e.

Русский

Операция согласования коммутирует с симметрией: congr e symm = (congr e).symm.

LaTeX

$$congr e).symm = congr e.symm$$

Lean4

theorem congr_congr (e : M' ≃ₗ[R] M'') (f : M ≃ₗ[R] M') (B : BilinForm R M) :
    congr e (congr f B) = congr (f.trans e) B :=
  rfl

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

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

Разделы

Аффилиация

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