Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 20:30 8430aae3

View on Github →

feat(algebra/group_power/lemmas): More lemmas through to_additive (#13537) Use to_additive to generate a bunch of old nsmul/zsmul lemmas from new pow/zpow ones. Also protect nat.nsmul_eq_mul as it should have been.

Estimated changes

modified theorem commute.self_zpow
modified theorem commute.zpow_left
modified theorem commute.zpow_right
modified theorem commute.zpow_self
modified theorem commute.zpow_zpow_self
modified theorem semiconj_by.zpow_right
modified theorem abs_add_eq_add_abs_iff
modified theorem abs_add_eq_add_abs_le
modified theorem abs_nsmul
modified theorem abs_zsmul
modified theorem commute.cast_int_mul_right
modified theorem commute.self_cast_int_mul
modified theorem commute.self_cast_nat_mul
deleted theorem nsmul_le_nsmul_iff
deleted theorem nsmul_lt_nsmul_iff
added theorem one_lt_zpow'
added theorem zpow_eq_zpow_iff'
added theorem zpow_le_zpow'
added theorem zpow_le_zpow
added theorem zpow_le_zpow_iff'
added theorem zpow_le_zpow_iff
added theorem zpow_left_inj
added theorem zpow_left_injective
added theorem zpow_lt_zpow'
added theorem zpow_lt_zpow
added theorem zpow_lt_zpow_iff'
added theorem zpow_lt_zpow_iff
added theorem zpow_mono_left
added theorem zpow_mono_right
added theorem zpow_strict_mono_left
added theorem zpow_strict_mono_right
deleted theorem zsmul_eq_zsmul_iff'
deleted theorem zsmul_le_zsmul'
deleted theorem zsmul_le_zsmul
deleted theorem zsmul_le_zsmul_iff'
deleted theorem zsmul_le_zsmul_iff
deleted theorem zsmul_lt_zsmul'
deleted theorem zsmul_lt_zsmul
deleted theorem zsmul_lt_zsmul_iff'
deleted theorem zsmul_lt_zsmul_iff
deleted theorem zsmul_mono_left
deleted theorem zsmul_mono_right
modified theorem zsmul_one
deleted theorem zsmul_pos
deleted theorem zsmul_right_inj
deleted theorem zsmul_right_injective
deleted theorem zsmul_strict_mono_left
deleted theorem zsmul_strict_mono_right
added theorem pow_le_pow_iff'
added theorem pow_lt_pow_iff'
added theorem pow_strict_mono_left
deleted theorem nat.nsmul_eq_mul