isUnit_comp_symm_iff — Mathlib

English

Let M be as above. The is-unit property is preserved under the inverse block-map: IsUnit((compAlgEquiv I J R K).symm M) ↔ IsUnit M.

Русский

Пусть M определяется как выше. Свойство обратимости сохраняется при обратном блочном отображении: IsUnit((compAlgEquiv I J R K).symm M) ↔ IsUnit M.

LaTeX

$$$\\operatorname{IsUnit}(\\,(\\operatorname{compAlgEquiv}_{I,J,R,K})^{-1}\\,M) \\iff \\operatorname{IsUnit}(M)$$$

Lean4

@[simp]
theorem isUnit_comp_symm_iff {M : Matrix (I × J) (I × J) R} : IsUnit (comp _ _ _ _ _ |>.symm M) ↔ IsUnit M :=
  isUnit_map_iff (compAlgEquiv _ _ _ ℕ).symm M

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