separatingRight_iff_linear_flip_nontrivial

English

Left-separating property is equivalent to having trivial kernel.

Русский

Левое раздельное свойство эквивалентно тривиальному ядру.

LaTeX

$$$B.SeparatingLeft \\leftrightarrow \\ker B = \\{0\\}$$$

Lean4

theorem separatingRight_iff_linear_flip_nontrivial {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.SeparatingRight ↔ ∀ y : M₂, B.flip y = 0 → y = 0 := by
  rw [← flip_separatingLeft, separatingLeft_iff_linear_nontrivial]

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