Commit 2024-07-19 17:33 33834763
View on Github →feat: generalize Siegel's lemma to A = 0
(#14852)
The Wikipedia statement of Siegel's lemma did not contain the hypothesis A != 0
in the lean formalization. A slight variant of the statement is still true if A = 0
. The original statement is recovered under the assumption A != 0
.