eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero

English

If x lies in the root span and RootForm(x,x)=0, then x=0.

Русский

Если x лежит в корневом Span и RootForm(x,x)=0, то x=0.

LaTeX

$$x ∈ P.rootSpan R ∧ P.RootForm x x = 0 ⇒ x = 0$$

Lean4

theorem eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M} (hx : x ∈ P.rootSpan R) (hx' : P.RootForm x x = 0) :
    x = 0 :=
  by
  have : x ∈ P.rootSpan R ⊓ LinearMap.ker P.RootForm := ⟨hx, P.rootForm_self_eq_zero_iff.mp hx'⟩
  simpa [P.disjoint_rootSpan_ker_rootForm.eq_bot] using this

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