Topology instances matrix (contribution to mathlib)

Stream: new members

[Aron Erben]

Hello, I would like to add some instances to mathlib for matrices, as requested here.

I have a couple questions
1.) There is already a matrix.has_continuous_smul, which only applies to matrices where both indices have the same type. I've written an instance for arbitrary matrices, what should the name be? I could not find anything in the naming conventions regarding this case. Should It simply be matrix.has_continuous_smul'?

2.) I wanted to add

instance [has_add (matrix m n R)] : has_continuous_add (matrix m n R) :=
pi.has_continuous_add

However, I'm getting

58:1: type mismatch, term
  pi.has_continuous_add
has type
  has_continuous_add (Π (i : ?m_1), ?m_2 i)
but is expected to have type
  has_continuous_add (matrix m n R)

Turning the matrix into a function type with

instance [has_add (matrix m n R)] : has_continuous_add (matrix m n R) :=
by delta matrix; exact pi.has_continuous_add

gives

58:24: invalid type ascription, term has type
  has_continuous_add (Π (i : ?m_1), ?m_2 i)
but is expected to have type
  has_continuous_add (m → n → R)
state:
m : Type u_4,
n : Type u_5,
R : Type u_8,
_inst_2 : topological_space R,
_inst_3 : has_add (matrix m n R)
⊢ has_continuous_add (m → n → R)

I'm a bit confused as to why this happens, as I assumed function types are subtypes of pi types.

3.) Could someone invite me to mathlib so I can contribute these new instances? My GitHub name is aronerben. A bit of context/an introduction: I have little formal training in math, as I'm a software dev with a CS background :smile: . At my dayjob, I'm currently working on formalizing theorems from econometry in Lean as a long-term project with one of the professors at my department. So this means we are currently focusing on applied linear algebra, regressions, etc.

Thanks in advance!

[Eric Wieser]

I've sent you an invite!

[Eric Wieser]

This isn't the right statement:

instance [has_add (matrix m n R)] : has_continuous_add (matrix m n R) :=
pi.has_continuous_add

because it allows any possible definition of + on matrices. You want

instance [has_add R] [has_continuous_add R] : has_continuous_add (matrix m n R) :=
pi.has_continuous_add

[Eric Wieser]

There is already a docs#matrix.has_continuous_smul, which only applies to matrices where both indices have the same type.

Oops, that's my fault! Just replace the existing instance with the correct one

[Eric Wieser]

I was thinking about exponentials of square matrices at the time and forgot to write m n