eval_zpow'

Mathlib.Tactic.FieldSimp.Lemmas

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

Lean4

theorem eval_zpow' [CommGroupWithZero M] (l : NF M) (r : ℤ) : (l ^ r).eval = zpow' l.eval r :=
  by
  unfold NF.eval at ⊢
  simp only [zpow_apply, list_prod_zpow', map_map]
  congr! 2
  ext p
  simp [← zpow'_mul, mul_comm]

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

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

Разделы

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

Аффилиация

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