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.