nondegenerate_iff_separatingLeft — Mathlib

English

If the restriction of a symmetric, nondegenerate bilinear map B to a subspace W is nondegenerate, then W is disjoint from the kernel of B.

Русский

Если ограничение симметричной невырожденной билинейной формы B к подпространству W невырождено, то W и ядро B попарно не пересекаются.

LaTeX

$$Disjoint W (ker B) with Nondegenerate domRestrict$$

Lean4

theorem nondegenerate_iff_separatingLeft {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) :
    B.Nondegenerate ↔ B.SeparatingLeft :=
  by
  refine ⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩
  rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]
  rwa [← separatingLeft_iff_ker_eq_bot]

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