invertibleOfPos

Mathlib.Algebra.CharP.Invertible

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

English

In a semifield K with CharZero, every positive natural number n is invertible in K.

Русский

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

LaTeX

$$Invertible(n.cast) in K for all n with NeZero n$$

Lean4

instance invertibleOfPos [CharZero K] (n : ℕ) [NeZero n] : Invertible (n : K) :=
  invertibleOfNonzero <| NeZero.out

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

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

Разделы

Аффилиация

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