Zulip Chat Archive

Stream: new members

Topic: Topology instances matrix (contribution to mathlib)


Aron Erben (May 17 2022 at 15:09):

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 (May 17 2022 at 15:15):

I've sent you an invite!

Eric Wieser (May 17 2022 at 15:16):

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 (May 17 2022 at 15:16):

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 (May 17 2022 at 15:18):

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


Last updated: Dec 20 2023 at 11:08 UTC