A proof that characterizes when two linear maps have equal

Stream: new members

[Miraj Samarakkody]

Hi everyone! I’m Miraj, a researcher in differential geometry interested in formalizing mathematics in Lean. I’m currently working on a proof that characterizes when two linear maps have equal kernels (from Axler’s Linear Algebra Done Right). I’d like to contribute this to Mathlib if it’s not already there. Would this be a welcome addition?

This is my first project, and I’m mostly trying to learn Lean.

[Eric Wieser]

Could you share the statement of the theorem, either as Lean or $\LaTeX$?

[Eric Wieser]

Note that mathlib does not collect proofs, but statements; and so if the result is already in mathlib but proved via different means, mathlib isn't interested in having a second proof. On the other hand, if your proof holds for a more general statement, then mathlib will happily replace the previous one with yours!