zpow'

Mathlib.Tactic.FieldSimp.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.FieldSimp.zpow'

Lean4

/-- This is a variant of integer exponentiation, defined for internal use in the `field_simp` tactic
implementation. It differs from the usual integer exponentiation in that `0 ^ 0` is `0`, not `1`.
With this choice, the function `n ↦ a ^ n` is always a homomorphism (`a ^ (n + m) = a ^ n * a ^ m`),
even if `a` is zero. -/
noncomputable def zpow' (a : α) (n : ℤ) : α :=
  if a = 0 ∧ n = 0 then 0 else a ^ n

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

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

Разделы

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

Аффилиация

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