inv_mul_cancel

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.inv_mul_cancel

← MathLib Explorer

English

If the first component of x is nonzero, then x inverse times x equals 1.

Русский

Если первый компонент x не равен нулю, то x^{-1} x = 1.

LaTeX

$$$ fst(x) \\neq 0 \\Rightarrow x^{-1} \\cdot x = 1 $$$

Lean4

protected theorem inv_mul_cancel {x : tsze R M} (hx : fst x ≠ 0) : x⁻¹ * x = 1 :=
  by
  convert mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx) using 2
  ext <;> simp

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

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

Разделы

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

Аффилиация

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