Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-26 15:40 f1fba68d

View on Github →

feat(algebra): porting modules from lean2

Estimated changes

added theorem mul_smul
added theorem neg_smul
added theorem one_smul
added def ring.to_module
added theorem smul_left_distrib
added theorem smul_neg
added theorem smul_right_distrib
added theorem smul_sub_left_distrib
added theorem smul_zero
added theorem sub_smul_right_distrib
added theorem zero_smul