exists_coroot_ne — Mathlib

English

Coroot span and ker CorootForm are disjoint, i.e., their intersection is {0}.

Русский

Область коротов и ядро CorootForm пересекаются только в нулe, то есть ⟂ взаимно точны.

LaTeX

$$Disjoint (corootSpan R) (LinearMap.ker CorootForm)$$

Lean4

theorem exists_coroot_ne [P.IsAnisotropic] {x : P.rootSpan S} (hx : x ≠ 0) : ∃ i, P.coroot'In S i x ≠ 0 :=
  by
  have hI := P.polarizationIn_Injective S
  have h := (map_ne_zero_iff (P.PolarizationIn S) hI).mpr hx
  rw [PolarizationIn_apply] at h
  contrapose! h
  exact Fintype.sum_eq_zero (fun a ↦ (P.coroot'In S a) x • P.coroot a) fun i ↦ by simp [h i]

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