As for definitions: it looks like Alexander was referring mainly to $e-statements which serve the purpose of local definitions, while David talked mainly about the $a-statements. As for the $e-statement definitions, they can serve as definitions used in the statement of the theorem, or only in its proof. They can be removed easily: I added two theorems a few months ago to illustrate this: http://us2.metamath.org/mpeuni/bj-pwcfsdom.html http://us2.metamath.org/mpeuni/bj-grur1.html (the comment there should read "grur1" and not "grur1a") where I call these hypotheses respectively "definitional hypotheses" and "proof-facilitating hypotheses".
Alexander: it might be possible, similarly, to use one version of cayleyhamilton to prove the other, instead of having two very similar proofs. As for lemmas: I agree that they could be more used. It can even be rewarding to extract such lemmas. I experienced this recently after noticing that two proofs were nearly identical, and searching precisely what they had in common, before extracting it as a separate theorem (this is http://us2.metamath.org/ileuni/peano5set.html with its two uses). Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/79e706e9-4d13-42fa-9d1a-b1cc491c0bc0%40googlegroups.com.
