instNatPowAssoc — Mathlib

English

If each α_i is a MulOneClass with Pow by ℕ and NatPowAssoc, then the function space ∀ i, α_i has NatPowAssoc, i.e., the natural power laws hold componentwise.

Русский

Если для каждой i выполняется MulOneClass, есть Pow по ℕ и NatPowAssoc для α_i, то пространство функций ∀ i, α_i имеет NatPowAssoc, то есть законы натуральных степеней выполняются по компонентам.

LaTeX

$$$\text{NatPowAssoc}(\forall i, \alpha_i)$$$

Lean4

instance instNatPowAssoc {ι : Type*} {α : ι → Type*} [∀ i, MulOneClass <| α i] [∀ i, Pow (α i) ℕ]
    [∀ i, NatPowAssoc <| α i] : NatPowAssoc (∀ i, α i)
    where
  npow_add _ _ _ := by ext; simp [npow_add]
  npow_zero _ := by ext; simp
  npow_one _ := by ext; simp

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