invertibleSucc

Mathlib.Algebra.CharP.Invertible

URI: https://scilib.ai/kg/mathlib#invertibleSucc

English

In a DivisionSemiring K with CharZero, every successor n.succ is invertible in K.

Русский

В дивизионном полукольце K с CharZero каждый следующеe число n+1 обратимо в K.

LaTeX

$$Invertible((n.succ) : K)$$

Lean4

instance invertibleSucc (n : ℕ) : Invertible (n.succ : K) :=
  invertibleOfNonzero (Nat.cast_ne_zero.mpr (Nat.succ_ne_zero _))

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

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

Разделы

Аффилиация

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