Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 19:37 177b5eb0

View on Github →

feat(linear_algebra): dimension of the base field is 1

Estimated changes

Modified src/algebra/module.lean

Modified src/linear_algebra/basis.lean

added theorem is_basis_singleton_one

Modified src/linear_algebra/dimension.lean

added theorem dim_of_field