isUnit_of_left_inverse

Mathlib.LinearAlgebra.Matrix.SemiringInverse

URI: https://scilib.ai/kg/mathlib#Matrix.isUnit_of_left_inverse

English

If there exists B with B A = I, then A is a unit (invertible).

Русский

Если существует B такое, что B A = I, то A является единицей (обратим).

LaTeX

$$$\exists B: B A = I \Rightarrow A \text{ is a unit}$$$

Lean4

theorem isUnit_of_left_inverse (h : B * A = 1) : IsUnit A :=
  ⟨⟨A, B, mul_eq_one_comm.mp h, h⟩, rfl⟩

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

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

Разделы

Аффилиация

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