isNNRat_inv_pos

Mathlib.Tactic.NormNum.Inv

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

Lean4

theorem isNNRat_inv_pos {α} [DivisionSemiring α] [CharZero α] {a : α} {n d : ℕ} :
    IsNNRat a (Nat.succ n) d → IsNNRat a⁻¹ d (Nat.succ n) :=
  by
  rintro ⟨_, rfl⟩
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  exact ⟨this, by simp⟩

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

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

Разделы

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

Аффилиация

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