inv_smul'

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

URI: https://scilib.ai/kg/mathlib#Matrix.inv_smul'

English

For a unit k, (k • A)⁻¹ = k⁻¹ • A⁻¹.

Русский

Для единицы k: (k·A)⁻¹ = k⁻¹ · A⁻¹.

LaTeX

$$$k \in \alpha^{\times} \Rightarrow (k \cdot A)^{-1} = k^{-1} \cdot A^{-1}$ for IsUnit det A.$$

Lean4

theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹ :=
  inv_eq_left_inv (by simp [h, smul_smul])

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

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

Разделы

Аффилиация

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