congr_one

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

For f, g equivalences and elements m, n, congr f g acting on m ⊗ n yields f m ⊗ g n.

Русский

Для эквивалентностей f,g и элементов m,n congr f g действует на m ⊗ n как f m ⊗ g n.

LaTeX

$$$\mathrm{congr\_tmul} : \mathrm{congr} f g (m \otimes n) = f m \otimes g n$$$

Lean4

@[simp]
theorem congr_one : congr (1 : M ≃ₗ[A] M) (1 : N ≃ₗ[R] N) = 1 :=
  congr_refl

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

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

Разделы

Аффилиация

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