selfZPow_zero

Mathlib.RingTheory.Localization.Away.Basic

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

English

The selfZPow at exponent 0 is the multiplicative identity 1 in the localization.

Русский

SelfZPow при показательe 0 равен единице в локализации.

LaTeX

$$$selfZPow\ x\ B\ 0 = 1$$$

Lean4

@[simp]
theorem selfZPow_zero : selfZPow x B 0 = 1 := by simp [selfZPow_of_nonneg _ _ le_rfl]

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

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

Разделы

Аффилиация

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