Math is not about the definitions. It is about the connections between these definitions. And the techniques used to establish broader classes of connections between similar objects.
The way we formalize a connection is with a proof. And if the proof is "nice and modular" it sorta explains by itself how it can be used for similar problems.
And such proofs definitely belong into MathLib. There is often value in actually reading the Lean proof script (especially with the IDE support like jump to definition). It is not only there for the machine.
The way we formalize a connection is with a proof. And if the proof is "nice and modular" it sorta explains by itself how it can be used for similar problems.
And such proofs definitely belong into MathLib. There is often value in actually reading the Lean proof script (especially with the IDE support like jump to definition). It is not only there for the machine.