Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-02 10:18 f5f879e2

View on Github →

feat(linear_algebra/dimension): linear equiv iff eq dim (#5559) See related zulip discussion https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275

Estimated changes

Modified src/linear_algebra/basis.lean

deleted def equiv_of_is_basis'

deleted def equiv_of_is_basis

deleted theorem equiv_of_is_basis_comp

deleted theorem equiv_of_is_basis_refl

deleted theorem equiv_of_is_basis_symm_trans

deleted theorem equiv_of_is_basis_trans_symm

added def linear_equiv_of_is_basis'

added def linear_equiv_of_is_basis

added theorem linear_equiv_of_is_basis_comp

added theorem linear_equiv_of_is_basis_refl

added theorem linear_equiv_of_is_basis_symm_trans

added theorem linear_equiv_of_is_basis_trans_symm

Modified src/linear_algebra/dimension.lean

added theorem linear_equiv.lift_dim_eq

added theorem linear_equiv.nonempty_equiv_iff_dim_eq

added theorem linear_equiv.nonempty_equiv_iff_lift_dim_eq

added def linear_equiv.of_dim_eq

added def linear_equiv.of_lift_dim_eq

added theorem nonempty_linear_equiv_of_dim_eq

added theorem nonempty_linear_equiv_of_lift_dim_eq

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.nonempty_linear_equiv_iff_findim_eq

added theorem finite_dimensional.nonempty_linear_equiv_of_findim_eq

Modified src/linear_algebra/matrix.lean