Commit 2023-04-28 10:54 9e33075c

View on Github →

feat: port LinearAlgebra.Matrix.ZPow (#3671)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/ZPow.lean

added theorem IsUnit.det_zpow

added theorem Matrix.Commute.mul_zpow

added theorem Matrix.Commute.self_zpow

added theorem Matrix.Commute.zpow_left

added theorem Matrix.Commute.zpow_right

added theorem Matrix.Commute.zpow_self

added theorem Matrix.Commute.zpow_zpow

added theorem Matrix.Commute.zpow_zpow_self

added theorem Matrix.SemiconjBy.zpow_right

added theorem Matrix.coe_units_zpow

added theorem Matrix.conjTranspose_zpow

added theorem Matrix.inv_pow'

added theorem Matrix.inv_zpow'

added theorem Matrix.inv_zpow

added theorem Matrix.isUnit_det_zpow_iff

added theorem Matrix.one_div_pow

added theorem Matrix.one_div_zpow

added theorem Matrix.one_zpow

added theorem Matrix.pow_inv_comm'

added theorem Matrix.pow_sub'

added theorem Matrix.transpose_zpow

added theorem Matrix.zero_zpow

added theorem Matrix.zero_zpow_eq

added theorem Matrix.zpow_add

added theorem Matrix.zpow_add_of_nonneg

added theorem Matrix.zpow_add_of_nonpos

added theorem Matrix.zpow_add_one

added theorem Matrix.zpow_add_one_of_ne_neg_one

added theorem Matrix.zpow_bit0'

added theorem Matrix.zpow_bit0

added theorem Matrix.zpow_bit1'

added theorem Matrix.zpow_bit1

added theorem Matrix.zpow_coe_nat

added theorem Matrix.zpow_mul'

added theorem Matrix.zpow_mul

added theorem Matrix.zpow_ne_zero_of_isUnit_det

added theorem Matrix.zpow_neg

added theorem Matrix.zpow_neg_coe_nat

added theorem Matrix.zpow_neg_mul_zpow_self

added theorem Matrix.zpow_neg_one

added theorem Matrix.zpow_one_add

added theorem Matrix.zpow_sub

added theorem Matrix.zpow_sub_one