separatingRight_iff_flip_ker_eq_bot

English

Same content as the previous item: right-separating iff flip has trivial kernel.

Русский

Содержимое аналогично предыдущему: правое разделяющее ⇔ перевёрнутое ядро тривиально.

LaTeX

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

Lean4

/-- A bilinear map is right-separating if and only if its flip has a trivial kernel. -/
theorem separatingRight_iff_flip_ker_eq_bot {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.SeparatingRight ↔ LinearMap.ker B.flip = ⊥ := by rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]

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