inv_zero

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.inv_zero

← MathLib Explorer

English

For all n, the inverse of 0 in ZMod n is 0: 0⁻¹ = 0.

Русский

Для любого n обратное нулю в ZMod n равно нулю: 0⁻¹ = 0.

LaTeX

$$$ (0 : ZMod n)^{-1} = 0 $$$

Lean4

theorem inv_zero : ∀ n : ℕ, (0 : ZMod n)⁻¹ = 0
  | 0 => Int.sign_zero
  | n + 1 =>
    show (Nat.gcdA _ (n + 1) : ZMod (n + 1)) = 0 by
      rw [val_zero]
      unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
      rfl

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

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

Разделы

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

Аффилиация

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