Commit 2024-07-05 15:12 1e27b81f

View on Github →

feat: Cardinal of GLn with coefficients in a finite field (#14095)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added def equiv_linearIndependent

Created Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean

added theorem Matrix.card_GL_field

added theorem card_linearIndependent