inv_mul

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.inv_mul

English

If a p-adic element z has norm 1, then z^{-1} exists and z^{-1} z = 1.

Русский

Если у z в p‑адических числах нормa равна 1, то z^{-1} существует и z^{-1} z = 1.

LaTeX

$$z^{-1} \cdot z = 1 \\text{ whenever } \|z\| = 1$$

Lean4

theorem inv_mul {z : ℤ_[p]} (hz : ‖z‖ = 1) : z.inv * z = 1 := by rw [mul_comm, mul_inv hz]

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

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

Разделы

Аффилиация

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