Theorem Matrix.kronecker_natCast

Modification history

2024-05-06 15:07

Mathlib/Data/Matrix/Kronecker.lean

feat: add `natCast` lemmas for `Matrix.kronecker` (#12703)

Added Matrix.kronecker_natCast View on Github →