instIsReducedForall — Mathlib

English

If every R_i is IsReduced, then the Pi-type ∀ i, R_i is IsReduced.

Русский

Если каждый R_i редуцирован, то пространственный тип функций ∀ i, R_i редуцирован.

LaTeX

$$IsReduced ((i : ι) → R i) if ∀ i, IsReduced (R i)$$

Lean4

instance (ι) (R : ι → Type*) [∀ i, Zero (R i)] [∀ i, Pow (R i) ℕ] [∀ i, IsReduced (R i)] : IsReduced (∀ i, R i) where
  eq_zero _ := fun ⟨n, hn⟩ ↦ funext fun i ↦ IsReduced.eq_zero _ ⟨n, congr_fun hn i⟩

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