Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-24 09:53 85636f9a

View on Github →

feat(data/complex|matrix): instances of star_ordered_ring and star_ordered_algebra (#4686)

Estimated changes

Modified src/analysis/quaternion.lean

deleted theorem quaternion.coe_complex_smul

added theorem quaternion.coe_real_complex_mul

Modified src/data/complex/basic.lean

added def complex.complex_star_ordered_ring

Modified src/data/complex/module.lean

added theorem complex.complex_ordered_semimodule

deleted theorem complex.im_smul

deleted theorem complex.re_smul

added theorem complex.smul_coe

Modified src/data/real/basic.lean