instPNatPowAssoc — Mathlib

English

If M and N have PNATPowAssoc, then M × N has PNATPowAssoc.

Русский

Если M и N имеют PNATPowAssoc, то произведение M × N имеет PNATPowAssoc.

LaTeX

$$$\\text{PNatPowAssoc}(M) \\land \\text{PNatPowAssoc}(N) \\Rightarrow \\text{PNatPowAssoc}(M \\times N)$$$

Lean4

instance instPNatPowAssoc {N : Type*} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] [Mul N] [Pow N ℕ+] [PNatPowAssoc N] :
    PNatPowAssoc (M × N) where
  ppow_add _ _ _ := by ext <;> simp [ppow_add]
  ppow_one _ := by ext <;> simp

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