prod_rootForm_smul_coroot_mem_range_domRestrict

English

Same as above but with domain restriction to rootSpan R.

Русский

То же самое, но с ограничением области определения до rootSpan R.

LaTeX

$$($\\prod_{a\\in ι} P.RootForm (P.root a) (P.root a)) \\cdot P.coroot i \\in \\operatorname{range}(P.Polarization.domRestrict (P.rootSpan R))$$$

Lean4

theorem prod_rootForm_smul_coroot_mem_range_domRestrict (i : ι) :
    (∏ a : ι, P.RootForm (P.root a) (P.root a)) • P.coroot i ∈
      LinearMap.range (P.Polarization.domRestrict (P.rootSpan R)) :=
  by
  obtain ⟨c, hc⟩ := Finset.dvd_prod_of_mem (fun a ↦ P.RootForm (P.root a) (P.root a)) (Finset.mem_univ i)
  rw [hc, mul_comm, mul_smul, rootForm_self_smul_coroot]
  refine LinearMap.mem_range.mpr ?_
  use ⟨c • 2 • P.root i, by aesop⟩
  simp

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