Commit 2024-05-06 15:07 89472cc1

View on Github →

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

Estimated changes

Modified Mathlib/Data/Matrix/Kronecker.lean

added theorem Matrix.kronecker_natCast

added theorem Matrix.kronecker_ofNat

added theorem Matrix.natCast_kronecker

added theorem Matrix.natCast_kronecker_natCast

added theorem Matrix.ofNat_kronecker