Timeout in Matrix Product

Stream: mathlib4

[Nick_adfor]

I've found that the complex definition of matrix product makes some easy linear algebra conclusion terrible to formalise. For example, the following one is just about checking the definition of Projection Matrix (Hermitian and Idempotent) but it will face timeout.

import Mathlib

variable {n : Type _} [Fintype n] [DecidableEq n] {𝕜 : Type _} [RCLike 𝕜]

theorem is_projection_of_hermitian_and_square_eq (B : Matrix n n 𝕜) :
    B.IsHermitian → (B * B = B) → (B.IsHermitian ∧ B * B = B) := by
  intro hHerm hIdem
  exact ⟨hHerm, hIdem⟩
--It cannot work because of timeout.

[Eric Wieser]

That doesn't give a timeout for me in the web editor

[Nick_adfor]

Well, the version change must fix something.

[Eric Wieser]

What version are you using?

[Nick_adfor]

v4.16.0

[Eric Wieser]

That's over 8 months old, and probably its not worth people on zulip diagnosing the issue vs you updating

[Nick_adfor]

So now Lean 4 Web : )

[Eric Wieser]

It's possible to use Lean 4.24.0 on your own computer too!