exists_form_eq_form_and_form_ne_zero

English

There exists k with B.form(P.root k, P.root k) = B.form(P.root j, P.root j) and B.form(P.root i, P.root k) ≠ 0.

Русский

Существует k такое, что B.form(P.root k, P.root k) = B.form(P.root j, P.root j) и B.form(P.root i, P.root k) ≠ 0.

LaTeX

$$$$ \exists k, \ B.form(P.root_k, P.root_k) = B.form(P.root_j, P.root_j) \ \land \ B.form(P.root_i, P.root_k) \neq 0. $$$$

Lean4

theorem exists_form_eq_form_and_form_ne_zero (B : P.InvariantForm) (i j : ι) :
    ∃ k, B.form (P.root k) (P.root k) = B.form (P.root j) (P.root j) ∧ B.form (P.root i) (P.root k) ≠ 0 :=
  by
  by_contra! contra
  suffices span R (orbit P.weylGroup (P.root j)) ≤ ker (B.form (P.root i)) from
    B.apply_root_ne_zero i <| by simpa [span_orbit_eq_top] using this
  refine span_le.mpr fun v hv ↦ ?_
  obtain ⟨g, rfl⟩ := mem_orbit_iff.mp hv
  simp only [P.weylGroup_apply_root, SetLike.mem_coe, LinearMap.mem_ker]
  apply contra
  simp [← Subgroup.smul_def g]

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