English
For a square matrix A, IsUnit((A^{z}).det) holds iff det(A) is a unit or z = 0. The determinant of z-pow is a unit exactly when either the original determinant is a unit or the exponent is zero.
Русский
Для квадратной матрицы A условие IsUnit((A^{z}).det) выполняется тогда, когда det(A) является единичным или z = 0. Детerminант z-повторения является единичным тогда, когда либо детерминант исходной матрицы — единичный, либо показатель z равен нулю.
LaTeX
$$$$\\IsUnit((A^{z}).\\det) \\iff (\\IsUnit(A.\\det) \\lor z=0).$$$$
Lean4
theorem isUnit_det_zpow_iff {A : M} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0 := by
induction z with
| zero => simp
| succ
z =>
rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj]
simp
| pred
z =>
rw [← neg_add', ← Int.natCast_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow, isUnit_pow_succ_iff,
neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
simp
