Right way to write identity Matrix?

Stream: lean4

[Mark Santa Clara Munro]

I'm getting the message "failed to synthesize OfNat (Matrix m n α) 1 numerals are polymorphic in Lean, but the numeral 1 cannot be used in a context where the expected type is Matrix m n α". I have tried using Matrix.one instead, but it is a different type. I have also tried to not include [Mul (Matrix m n α)] and the only reason I included [One α] [Zero α] was because I saw that it could help make it work. I'm assuming I am very wrong on something to do with types. I'm sorry if I am making a very obvious mistake, I tried to fix it for a while.

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m]

-- Operation which multiplies x by Row i
def mulRow [SMul R α] (M : Matrix m n α) (i : m) (x : R) : Matrix m n α :=
  Matrix.updateRow M i (x • M i)

-- Let Eix by the elementary matrix formed by multiplying Row i of the identity matrix by x
-- Here we show that multiplying Eix by M is the same as multiplying Row i of M by x
theorem mulRowMat_eq_mulRow [SMul R α] [Mul (Matrix m n α)] [One α] [Zero α] (M : Matrix m n α) (i : m) (x : R)
  : mulRow (1 : Matrix m n α) i x * M = mulRow M i x := by
  ext k l

[Ruben Van de Velde]

What's 1 supposed to mean?

[Damiano Testa]

What should 1 mean for a non-square matrix?

[Mark Santa Clara Munro]

What i wanted it to be is an identity matrix (square yes), I realize I did that wrong