instInvertibleInv

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

The nonsingular inverse equals invOf when A is invertible.

Русский

Несингобратная обратная равна invOf, если A обращима.

LaTeX

$$$A \\text{ invertible} \\Rightarrow A^{-1}_{\\mathrm{ns}} = \\mathrm{invOf}(A)$$$

Lean4

instance [Invertible A] : Invertible A⁻¹ := by
  rw [← invOf_eq_nonsing_inv]
  infer_instance

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

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

Разделы

Аффилиация

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