uzpow_zero

Mathlib.Data.ZMod.IntUnitsPower

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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