Commit 2020-06-09 21:53 4e1558bf

View on Github →

chore(algebra/group_power): simp attribute on nsmul_eq_mul and gsmul_eq_mul (#2983) Also fix the resulting lint failures, corresponding to the fact that several lemmas are not in simp normal form any more.

Estimated changes

Modified src/algebra/group_power.lean

added theorem commute.cast_int_mul_cast_int_mul

added theorem commute.cast_int_mul_left

added theorem commute.cast_int_mul_right

added theorem commute.cast_int_mul_self

added theorem commute.cast_nat_mul_cast_nat_mul

added theorem commute.cast_nat_mul_left

added theorem commute.cast_nat_mul_right

added theorem commute.cast_nat_mul_self

deleted theorem commute.gsmul_gsmul

deleted theorem commute.gsmul_left

deleted theorem commute.gsmul_right

deleted theorem commute.gsmul_self

deleted theorem commute.nsmul_left

deleted theorem commute.nsmul_nsmul

deleted theorem commute.nsmul_right

deleted theorem commute.nsmul_self

added theorem commute.self_cast_int_mul

added theorem commute.self_cast_int_mul_cast_int_mul

added theorem commute.self_cast_nat_mul

added theorem commute.self_cast_nat_mul_cast_nat_mul

deleted theorem commute.self_gsmul

deleted theorem commute.self_gsmul_gsmul

deleted theorem commute.self_nsmul

deleted theorem commute.self_nsmul_nsmul

modified theorem gsmul_eq_mul

modified theorem nat.nsmul_eq_mul

modified theorem nsmul_eq_mul

added theorem semiconj_by.cast_int_mul_cast_int_mul

added theorem semiconj_by.cast_int_mul_left

added theorem semiconj_by.cast_int_mul_right

added theorem semiconj_by.cast_nat_mul_cast_nat_mul

added theorem semiconj_by.cast_nat_mul_left

added theorem semiconj_by.cast_nat_mul_right

deleted theorem semiconj_by.gsmul_gsmul

deleted theorem semiconj_by.gsmul_left

deleted theorem semiconj_by.gsmul_right

deleted theorem semiconj_by.nsmul_left

deleted theorem semiconj_by.nsmul_nsmul

deleted theorem semiconj_by.nsmul_right

Modified src/analysis/special_functions/trigonometric.lean

deleted theorem real.angle.coe_gsmul

added theorem real.angle.coe_int_mul_eq_gsmul

added theorem real.angle.coe_nat_mul_eq_nsmul

deleted theorem real.angle.coe_smul

Modified src/data/real/nnreal.lean