uzpow_one

Mathlib.Data.ZMod.IntUnitsPower

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

English

For any s ∈ Units Int, s^1 = s.

Русский

Для любого s ∈ Units Int: s^1 = s.

LaTeX

$$$s^{1} = s.$$$

Lean4

@[simp]
theorem uzpow_one (s : ℤˣ) : (s ^ (1 : R) : ℤˣ) = s :=
  Additive.ofMul.injective <| one_smul R (Additive.ofMul s)

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

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

Разделы

Аффилиация

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