selfZPow_neg_natCast

Mathlib.RingTheory.Localization.Away.Basic

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

← MathLib Explorer

English

For natural d, selfZPow at -d equals mk' with 1 and x^d.

Русский

Для натурального d, selfZPow при -d равно mk' с 1 и x^d.

LaTeX

$$$selfZPow(x,B,-d) = mk'(B,1,Submonoid.pow(x,d))$$$

Lean4

@[simp]
theorem selfZPow_neg_natCast (d : ℕ) : selfZPow x B (-d) = mk' _ (1 : R) (Submonoid.pow x d) := by
  simp [selfZPow_of_nonpos _ _ (neg_nonpos.mpr (Int.natCast_nonneg d))]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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