prod_pow_mem_graded — Mathlib

English

If F is finite and n(k) is a natural number, and g(k) ∈ A(i(k)) for all k ∈ F, then the product ∏_{k∈F} g(k)^{n(k)} lies in A(∑_{k∈F} n(k) • i(k)).

Русский

Если F конечен и n(k) — неотрицательное целое, а элемент g(k) принадлежит A(i(k)) для каждого k ∈ F, то произведение ∏ g(k)^{n(k)} принадлежит A(∑ n(k) • i(k)).

LaTeX

$$$ \forall F : Finset κ, \forall n : κ \to \mathbb{N}, \ ((\forall k ∈ F, g(k) ∈ A(i(k)))) \Rightarrow \prod_{k ∈ F} g(k)^{n(k)} ∈ A\Big(\sum_{k ∈ F} n(k) \cdot i(k)\Big) $$$

Lean4

theorem prod_pow_mem_graded (n : κ → ℕ) (hF : ∀ k ∈ F, g k ∈ A (i k)) : ∏ k ∈ F, g k ^ n k ∈ A (∑ k ∈ F, n k • i k) :=
  prod_mem_graded A _ _ fun k hk ↦ pow_mem_graded _ (hF k hk)

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