speed up

Stream: new members

[vxctyxeha]

hello！ i try to prove the folloe but It seems that loading gets a bit slower when the data increases. Are there any methods to speed it up?

import Mathlib

-- Performance optimization settings for heavy matrix computations
open Matrix


theorem eq : Fintype.card {A : Matrix (Fin 3) (Fin 3) (ZMod 5) | A.det = 1 ∨ A.det = 2 ∨ A.det = 3 ∨ A.det = 4} = 1488000 := by

    native_decide

[Eric Wieser]

I would guess that simp_rw [Matrix.det_fin_three] speeds it up a little

[Eric Wieser]

theorem eq : Finset.card {A : Matrix (Fin 3) (Fin 3) (ZMod 5) | A.det ∈ ({1, 2, 3, 4} : Finset _)} = 1488000 := by
  simp_rw [Matrix.det_fin_three]
  native_decide

is probably even faster

[vxctyxeha]

(deleted)