eval_cons_of_pow_eq_zero

Mathlib.Tactic.FieldSimp.Lemmas

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

Lean4

theorem eval_cons_of_pow_eq_zero [CommGroupWithZero M] {r : ℤ} (hr : r = 0) {x : M} (hx : x ≠ 0) (l : NF M) :
    ((r, x) ::ᵣ l).eval = NF.eval l := by simp [hr, zpow'_zero_of_ne_zero hx]

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

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

Разделы

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

Аффилиация

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