instNatPowAssoc — Mathlib

English

If M and N have NatPowAssoc, then the product M × N has NatPowAssoc, i.e., exponent laws hold componentwise.

Русский

Если M и N имеют NatPowAssoc, то произведение M × N имеет NatPowAssoc, т.е. законы степеней выполняются по компонентам.

LaTeX

$$$\NatPowAssoc(M \times N)$$$

Lean4

instance instNatPowAssoc {N : Type*} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] [MulOneClass N] [Pow N ℕ]
    [NatPowAssoc N] : NatPowAssoc (M × N)
    where
  npow_add _ _ _ := by ext <;> simp [npow_add]
  npow_zero _ := by ext <;> simp
  npow_one _ := by ext <;> simp

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