SeparatingLeft — Mathlib

English

In a nontrivial module, the zero bilinear form cannot be separating on the left.

Русский

В ненулевом модуле нулевая билинейная форма не может быть лево‑разделяющей.

LaTeX

$$[Nontrivial M₁] → (SeparatingLeft 0) is false$$

Lean4

/-- A bilinear map is called left-separating if
the only element that is left-orthogonal to every other element is `0`; i.e.,
for every nonzero `x` in `M₁`, there exists `y` in `M₂` with `B x y ≠ 0`. -/
def SeparatingLeft (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) : Prop :=
  ∀ x : M₁, (∀ y : M₂, B x y = 0) → x = 0

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