separatingLeft_iff_ker_eq_bot — Mathlib

English

A bilinear form is right-separating iff the kernel of its flip is trivial.

Русский

Правая разделяющая билинейная форма эквивалентна тому, что ядро её перевёрнутой формы тривиально.

LaTeX

$$$B.SeparatingRight \\leftrightarrow ker(B^{\\mathrm{flip}}) = \\{0\\}$$$

Lean4

/-- A bilinear map is left-separating if and only if it has a trivial kernel. -/
theorem separatingLeft_iff_ker_eq_bot {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} : B.SeparatingLeft ↔ LinearMap.ker B = ⊥ :=
  Iff.trans separatingLeft_iff_linear_nontrivial LinearMap.ker_eq_bot'.symm

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