inv_smul — Mathlib

English

For A and scalar k with invertible k, (k • A)⁻¹ = ⅟k • A⁻¹ whenever det A is a unit.

Русский

Для матрицы A и скаляра k, удовлетворяющего условиям обратимости, (k·A)⁻¹ = k⁻¹ · A⁻¹ при условии, что det A единичен.

LaTeX

$$$\forall k \; [Invertible k] \; (\det A) \in U \Rightarrow (k \cdot A)^{-1} = k^{-1} \cdot A^{-1}$.$$

Lean4

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

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