prod_rootFormIn_smul_coroot_mem_range_PolarizationIn

English

The product over j of RootForm values times coroots, acting on a fixed coroot i, lies in the range of PolarizationIn.

Русский

Произведение значений RootForm по j, умноженных на корootы, действующее на фиксированный i, лежит в диапазоне PolarizationIn.

LaTeX

$$$\\bigl(\\prod_{j \\in ι} P.RootForm (P.root j) (P.root j)\\bigr) \\cdot P.coroot i \\in \\operatorname{range}(P.PolarizationIn S)$$$

Lean4

theorem prod_rootFormIn_smul_coroot_mem_range_PolarizationIn (i : ι) :
    (∏ j : ι, P.RootFormIn S (P.rootSpanMem S j) (P.rootSpanMem S j)) • P.coroot i ∈
      LinearMap.range (P.PolarizationIn S) :=
  by
  obtain ⟨c, hc⟩ :=
    Finset.dvd_prod_of_mem (fun j ↦ P.RootFormIn S (P.rootSpanMem S j) (P.rootSpanMem S j)) (Finset.mem_univ i)
  rw [hc, mul_comm, mul_smul, rootFormIn_self_smul_coroot]
  refine LinearMap.mem_range.mpr ?_
  use c • 2 • (P.rootSpanMem S i)
  rw [map_smul, two_smul, two_smul, map_add]

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