ext_iff₂

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.ext_iff₂

English

Flipping the order of arguments in a bilinear map swaps the arguments.

Русский

Переключение порядка аргументов в билинейном отображении меняет местами аргументы.

LaTeX

$$$$ flip (f) n m = f m n $$$$

Lean4

theorem ext_iff₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ m n, f m n = g m n :=
  ⟨congr_fun₂, ext₂⟩

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

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

Разделы

Аффилиация

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