ofAdd_mul — Mathlib

English

Let a and b be integers with a interpreted in the additive sense and b as an exponent; the relation between multiplication and exponentiation under the additive–multiplicative correspondence is given by the identity: ofAdd (a * b) = ofAdd a ^ b.

Русский

Пусть a и b — целые числа; в рамках аддитивно-мультипликативного соответствия имеет место равенство: ofAdd(a · b) = (ofAdd a)^b.

LaTeX

$$$ \operatorname{ofAdd}(a \cdot b) = (\operatorname{ofAdd}(a))^{\,b} $$$

Lean4

@[simp]
theorem ofAdd_mul (a b : ℤ) : ofAdd (a * b) = ofAdd a ^ b :=
  (toAdd_zpow ..).symm

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