isSymm_iff_eq_flip — Mathlib

English

The symmetry of a bilinear map is equivalent to equality with its flip.

Русский

Симметрия билинейной карты эквивалентна равенству с её перестановкой аргументов.

LaTeX

$$$\\text{BilinMap.isSymm_iff_eq_flip}: (B.IsSymm) \\iff (B = B.flip)$$$

Lean4

theorem isSymm_iff_eq_flip {N : Type*} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinMap R M N} :
    (∀ x y, B x y = B y x) ↔ B = B.flip := by simp [LinearMap.ext_iff₂]

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