Which file I need to import for Matrix multiplication?

Stream: mathlib4

[Hyunwoo Lee]

import Mathlib.LinearAlgebra.Matrix.Defs
import Mathlib.Data.Real.Basic

open Matrix

def mat_mul
  (A : Matrix (Fin 3) (Fin 3) ℝ)
  (B : Matrix (Fin 3) (Fin 3) ℝ)
:= A*B

This simple code fails because it cannot synthesize the instance HMul of given type Matrix (Fin 3) (Fin 3) ℝ. Ofcourse, if I import full Mathlib, it success, but I don't want to do it.

I search in Mathlib database and expect something like HMul (Matrix A B C) (Matrix B D C) (Matrix A D C) exists but I cannot find it...

[Robin Arnez]

You can import all of mathlib and then put #min_imports at the bottom of your file

[Robin Arnez]

import Mathlib

open Matrix

def mat_mul
  (A : Matrix (Fin 3) (Fin 3) ℝ)
  (B : Matrix (Fin 3) (Fin 3) ℝ)
:= A*B

/--
info: import Mathlib.Data.Matrix.Mul
import Mathlib.Data.Real.Basic
-/
#guard_msgs in
#min_imports

Seems like Mathlib.Data.Matrix.Mul is what you need here

[Hyunwoo Lee]

Thank you so much. You save me.

instance Matrix.instHMulOfFintypeOfMulOfAddCommMonoid , that's what I want.

But I still have two other questions.

1. Doesn't #min_imports still make automation tactic like aesop bit slower while writing the proof interactively? That's the biggest reason I don't want to import Mathlib.
2. I can't distinguish the definition in Mathlib.Data, and one in each module, such as Mathlib.LinearAlgebra. Is there a convention, or at least intuition about location of definition in Mathlib?

[Kevin Buzzard]

When developing I always import mathlib, I minimise imports at the end. I don't care where things are (unless I'm trying to add to mathlib, then I have to learn)