inv_eq_of_mul_eq_one

Mathlib.Data.ZMod.Basic

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

← MathLib Explorer

English

If a,b ∈ ZMod n satisfy a · b = 1, then a⁻¹ = b.

Русский

Если элементы a, b в ZMod n удовлетворяют a · b = 1, тогда a⁻¹ = b.

LaTeX

$$$a \cdot b = 1 \Rightarrow a^{-1} = b$$$

Lean4

protected theorem inv_eq_of_mul_eq_one (n : ℕ) (a b : ZMod n) (h : a * b = 1) : a⁻¹ = b :=
  left_inv_eq_right_inv (inv_mul_of_unit a ⟨⟨a, b, h, mul_comm a b ▸ h⟩, rfl⟩) h

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

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

Разделы

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

Аффилиация

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