congr_refl

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.congr_refl

English

Symmetry of congruence: congr f.symm g.symm = (congr f g).symm.

Русский

Симметрия конгруэнтности: congr f.symm g.symm = (congr f g).symm.

LaTeX

$$$\mathrm{congr\_symm} : \mathrm{congr}(f^{-1}, g^{-1}) = (\mathrm{congr}(f,g))^{-1}$$$

Lean4

@[simp]
theorem congr_refl : congr (.refl A M) (.refl R N) = .refl A _ :=
  LinearEquiv.toLinearMap_injective <| map_id

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

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

Разделы

Аффилиация

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