instPNatPowAssoc — Mathlib

English

If for each index i, α_i has PNATPowAssoc, then the product type ∀i, α_i has PNATPowAssoc.

Русский

Если для каждого индекса i у α_i есть PNATPowAssoc, то тип ∀i α_i имеет PNATPowAssoc.

LaTeX

$$$\\bigwedge_{i} \\text{PNatPowAssoc}(\\alpha_i) \\Rightarrow \\text{PNatPowAssoc}\\Big(\\prod_{i} \\alpha_i\\Big)$$$

Lean4

instance instPNatPowAssoc {ι : Type*} {α : ι → Type*} [∀ i, Mul <| α i] [∀ i, Pow (α i) ℕ+] [∀ i, PNatPowAssoc <| α i] :
    PNatPowAssoc (∀ i, α i) where
  ppow_add _ _ _ := by ext; simp [ppow_add]
  ppow_one _ := by ext; simp

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