nonneg_to_eq

Mathlib.Tactic.NormNum.Result

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.IsInt.nonneg_to_eq

Lean4

theorem nonneg_to_eq {α} [Ring α] {n} {a a' : α} (h : IsInt a (.ofNat n)) (e : n = a') : a = a' :=
  h.to_isNat.to_eq e

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

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

Разделы

Аффилиация

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