Theorem exists_basis_of_pairing_ne_zero

Modification history

2026-01-23 16:59
Mathlib/LinearAlgebra/Basis/VectorSpace.lean
feat(LinearAlgebra/Transvection): the determinant of a transvection is equal to 1. (#32757) …
Added exists_basis_of_pairing_ne_zeroView on Github →