PowAssoc — Mathlib

English

Every Monoid M satisfies NatPowAssoc, with npow_add = pow_add, npow_zero = pow_zero, and npow_one = pow_one.

Русский

Любой моноид M удовлетворяет NatPowAssoc, т.е. выполняются равенства npow_add = pow_add, npow_zero = pow_zero, и npow_one = pow_one.

LaTeX

$$$\text{NatPowAssoc}(M)$$$

Lean4

instance PowAssoc : NatPowAssoc M where
  npow_add _ _ _ := pow_add _ _ _
  npow_zero _ := pow_zero _
  npow_one _ := pow_one _

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