Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-20 13:15 8489972a

View on Github →

feat(data/complex/module): ![1, I] is a basis of C over R (#4713)

Estimated changes

Modified src/data/complex/module.lean

added theorem complex.coe_algebra_map

added theorem complex.dim_real_complex

added theorem complex.findim_real_complex

added theorem complex.im_smul

added theorem complex.is_basis_one_I

added theorem complex.re_smul

added theorem complex.{u}

added theorem dim_real_of_complex

added theorem findim_real_of_complex

Modified src/data/matrix/notation.lean

added theorem matrix.range_cons

added theorem matrix.range_empty