zpow'_zero_eq_div

Mathlib.Tactic.FieldSimp.Lemmas

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

Lean4

theorem zpow'_zero_eq_div (a : α) : zpow' a 0 = a / a :=
  by
  simp [zpow']
  by_cases h : a = 0
  · simp [h]
  · simp [h]

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

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

Разделы

Аффилиация

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