Commit 2024-05-24 08:18 72430e23
View on Github →fix(LinearAlgebra/BilinearForm/Orthogonal): fix name of restrict_nondegenerate_of_isCompl_orthogonal (#13157)
The lemma is renamed to the correct isCompl_orthogonal_of_restrict_nondegenerate and we add
alias restrict_nondegenerate_of_isCompl_orthogonal := isCompl_orthogonal_of_restrict_nondegenerate