list_prod_ofFn_mem_graded — Mathlib

English

For a finite n, and i: Fin n → ι, r: Fin n → R with r j ∈ A (i j), then (List.ofFn r).prod ∈ A (List.ofFn i).sum.

Русский

Для конечного n и отображений i и r, если r j ∈ A (i j), то произведение List.ofFn r принадлежит A (List.ofFn i).sum.

LaTeX

$$$ (List.ofFn r).prod \\in A (List.ofFn i).sum $$$

Lean4

theorem list_prod_ofFn_mem_graded {n} (i : Fin n → ι) (r : Fin n → R) (h : ∀ j, r j ∈ A (i j)) :
    (List.ofFn r).prod ∈ A (List.ofFn i).sum :=
  by
  rw [List.ofFn_eq_map, List.ofFn_eq_map]
  exact list_prod_map_mem_graded _ _ _ fun _ _ => h _

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