pi — Mathlib · SciLib

English

If each f_i is IsSmulRegular by k, then the product ∀ i, f_i is IsSmulRegular by k; i.e., regularity is preserved under product.

Русский

Если для всех i модулe f_i имеет IsSmulRegular по k, то произведение (i → f_i) также имеет IsSmulRegular по k; то есть регулярность сохраняется в произведении.

LaTeX

$$$\\big( \\forall i,\\ IsSMulRegular (f i)\\ k \\big) \\Rightarrow IsSMulRegular (\\forall i, f i) k.$$$

Lean4

theorem _root_.IsSMulRegular.pi {α : Type*} [∀ i, SMul α <| f i] {k : α} (hk : ∀ i, IsSMulRegular (f i) k) :
    IsSMulRegular (∀ i, f i) k := fun _ _ h => funext fun i => hk i (congr_fun h i :)

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