Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-04 04:40 1cfdf5f3

View on Github →

chore(linear_algebra/*): Lint (#16362) Satisfy the fintype_finite and fails_quickly linters.

Estimated changes

modified theorem linear_map.det_zero'
modified theorem dim_pi
modified theorem basis.coe_dual_basis
modified def basis.dual_basis
modified theorem basis.dual_basis_apply
modified theorem basis.dual_basis_apply_self
modified theorem basis.dual_basis_repr
modified theorem basis.dual_dim_eq
modified def basis.eval_equiv
modified theorem basis.eval_range
modified def basis.to_dual_equiv
modified theorem basis.to_dual_range
modified theorem basis.to_dual_to_dual
modified theorem basis.total_coord
modified theorem basis.total_dual_basis
modified theorem module.finite.of_basis
modified theorem module.free.rank_matrix''
modified theorem module.free.rank_matrix'
modified theorem module.free.rank_matrix
modified theorem matrix.finrank_matrix
modified theorem basis.ext_multilinear