Commit 2025-12-19 16:47 2ef954a5

chore: clean up imports from #31746 (#32657) #31746 added Data.Int.Cast.Lemmas as a new import to LinearAlgebra.Matrix.Diagonal to access Int.cast_ite but did not remove Data.Int.Cast.Basic and did not do a public import. Following Nat.cast_ite, we move Data.Int.Cast.Basic and remove the added import.