English
For any square matrix A, if det(A) is a unit then det(A^{n}) is a unit for all n ∈ ℤ.
Русский
Для любой квадратной матрицы A, если det(A) единичен, то det(A^{n}) единичен для всех n ∈ ℤ.
LaTeX
$$$$\\det(A^{n}) \\in \\mathbb{R}^{\\times} \\quad (n\\in\\mathbb{Z}).$$$$
Lean4
theorem zpow_right {A X Y : M} (hx : IsUnit X.det) (hy : IsUnit Y.det) (h : SemiconjBy A X Y) :
∀ m : ℤ, SemiconjBy A (X ^ m) (Y ^ m)
| (n : ℕ) => by simp [h.pow_right n]
| -[n+1] =>
by
have hx' : IsUnit (X ^ n.succ).det := by
rw [det_pow]
exact hx.pow n.succ
have hy' : IsUnit (Y ^ n.succ).det := by
rw [det_pow]
exact hy.pow n.succ
rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
refine (isRegular_of_isLeftRegular_det hy'.isRegular.left).left ?_
dsimp only
rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, mul_smul, mul_adjugate, ← Matrix.mul_assoc,
mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R), mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul, hy'.val_inv_mul,
one_smul, Matrix.mul_one, Matrix.one_mul]
