uzpow_mul — Mathlib

English

Let s be a unit in the integers and x,y be elements of a commutative semiring R equipped with a compatible additive action of the units. Then s^(x·y) = (s^x)^y.

Русский

Пусть s — элемент обратимый в целых числах и x,y — элементы кольца R с совместной с единицами надлежащей действием. Тогда s^(x·y) = (s^x)^y.

LaTeX

$$$ \forall s \in \mathbb{Z}^{\times}, \forall x,y \in R,\ s^{xy} = (s^{x})^{y} $$$

Lean4

theorem uzpow_mul (s : ℤˣ) (x y : R) : s ^ (x * y) = (s ^ x) ^ y :=
  Additive.ofMul.injective <| mul_comm x y ▸ mul_smul y x (Additive.ofMul s)

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