Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 11:33 c0dbe14d

View on Github →

feat(linear_algebra/matrix/fpow): integer powers of matrices (#8683) Since we have an inverse defined for matrices via nonsing_inv, we provide a div_inv_monoid instance for matrices. The instance provides the ability to refer to integer power of matrices via the auto-generated gpow. This is done in a new file to allow selective use. Many API lemmas are provided to facilitate usage of the new gpow, many copied in form/content from algebra/group_with_zero/power.lean, which provides a similar API.

Estimated changes

added theorem is_unit.det_fpow
added theorem matrix.fpow_add
added theorem matrix.fpow_add_one
added theorem matrix.fpow_bit0'
added theorem matrix.fpow_bit0
added theorem matrix.fpow_bit1'
added theorem matrix.fpow_bit1
added theorem matrix.fpow_coe_nat
added theorem matrix.fpow_mul'
added theorem matrix.fpow_mul
added theorem matrix.fpow_neg
added theorem matrix.fpow_neg_one
added theorem matrix.fpow_one_add
added theorem matrix.fpow_sub
added theorem matrix.fpow_sub_one
added theorem matrix.inv_fpow'
added theorem matrix.inv_fpow
added theorem matrix.inv_pow'
added theorem matrix.one_div_fpow
added theorem matrix.one_div_pow
added theorem matrix.one_fpow
added theorem matrix.pow_inv_comm'
added theorem matrix.pow_sub'
added theorem matrix.units.coe_fpow
added theorem matrix.units.coe_inv''
added theorem matrix.zero_fpow
added theorem matrix.zero_fpow_eq