isUnit_inv

Mathlib.Data.ZMod.Units

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

← MathLib Explorer

English

If n is a unit in ZMod m, then its inverse is also a unit.

Русский

Если n является единицей в ZMod m, то её обратное тоже единица.

LaTeX

$$$$ \\text{If } IsUnit(n: ZMod m) \\text{ then } IsUnit((n: ZMod m)^{-1}). $$$$

Lean4

theorem isUnit_inv {m : ℕ} {n : ℤ} (h : IsUnit (n : ZMod m)) : IsUnit (n : ZMod m)⁻¹ :=
  by
  rw [isUnit_iff_exists]
  exact ⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩

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

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

Разделы

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

Аффилиация

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