Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-30 14:17 374c290e

View on Github →

chore(linear_algebra): continue removing decidable_eq assumptions (#1404)

  • chore(linear_algebra): continue remocing decidable_eq assumptions
  • chore(data/mv_polynomial): get rid of unnecessary changes to instance depth
  • fix build
  • change class instance depth
  • class_instance depth t Please enter the commit message for your changes. Lines starting
  • delete some more decidable_eq
  • Update finite_dimensional.lean
  • Update finite_dimensional.lean
  • Update finite_dimensional.lean

Estimated changes

modified theorem constr_smul
modified theorem is_basis_singleton_one
modified theorem pi.is_basis_std_basis
modified theorem dim_quotient
modified theorem dim_span
modified theorem dim_span_set
modified theorem exists_is_basis_fintype
modified theorem is_basis.le_span
modified theorem is_basis.mk_eq_dim
modified theorem is_basis.mk_range_eq_dim
modified theorem linear_equiv.dim_eq_lift
modified theorem mk_eq_mk_of_basis
modified theorem finite_dimensional.of_fg
modified def lin_equiv_matrix'
modified def lin_equiv_matrix
modified theorem matrix.rank_diagonal
modified theorem to_matrix_to_lin