Theorem Matrix.zpow_neg_coe_nat

Modification history

2024-04-07 17:47

Mathlib/LinearAlgebra/Matrix/ZPow.lean

chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …

Deleted Matrix.zpow_neg_coe_nat View on Github →

2023-04-28 10:54

Mathlib/LinearAlgebra/Matrix/ZPow.lean

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

Added Matrix.zpow_neg_coe_nat View on Github →