ofMul_uzpow

Mathlib.Data.ZMod.IntUnitsPower

URI: https://scilib.ai/kg/mathlib#ofMul_uzpow

English

For any u ∈ ℤˣ and r ∈ R, Additive.ofMul (u^r) = r • Additive.ofMul u.

Русский

Для любого u ∈ ℤˣ и r ∈ R: Additive.ofMul (u^r) = r • Additive.ofMul u.

LaTeX

$$$Additive.ofMul (u^r) = r \cdot Additive.ofMul(u).$$$

Lean4

@[simp]
theorem ofMul_uzpow (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru