isUnit_comp_iff — Mathlib

English

Let M be a matrix in Matrix I I (Matrix J J R). Then IsUnit (comp M) is equivalent to IsUnit M; i.e., invertibility is preserved by the block composition map.

Русский

Пусть M ∈ Matrix I I (Matrix J J R). Тогда IsUnit (comp M) эквивалентно IsUnit M; то есть обратимость сохраняется при блочной композиционной карте.

LaTeX

$$$\\operatorname{IsUnit}(\\operatorname{comp}_{I,I,J,J,R}(M)) \\iff \\operatorname{IsUnit}(M)$$$

Lean4

@[simp]
theorem isUnit_comp_iff {M : Matrix I I (Matrix J J R)} : IsUnit (comp _ _ _ _ _ M) ↔ IsUnit M :=
  isUnit_map_iff (compAlgEquiv _ _ _ ℕ) M

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