Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-31 21:33 c91e6c2e

View on Github →

fix(ring_theory/algebra): remove duplicate theorems to fix build

Estimated changes

deleted theorem complex.smul_im:
deleted theorem complex.smul_re: