Commit 2023-10-30 16:19 dcc69c71

View on Github →

chore: split GroupPower/Order (#7978)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupPower/CovariantClass.lean

added theorem Left.one_le_pow_of_le

added theorem Left.pow_le_one_of_le

added theorem Left.pow_lt_one_iff'

added theorem Left.pow_lt_one_iff

added theorem Left.pow_lt_one_of_lt

added theorem Monotone.pow_right

added theorem Right.one_le_pow_of_le

added theorem Right.pow_le_one_of_le

added theorem Right.pow_lt_one_iff

added theorem Right.pow_lt_one_of_lt

added theorem StrictMono.pow_right'

added theorem le_max_of_sq_le_mul

added theorem le_of_pow_le_pow'

added theorem lt_max_of_sq_lt_mul

added theorem lt_of_pow_lt_pow'

added theorem min_le_of_mul_le_sq

added theorem min_lt_of_mul_lt_sq

added theorem one_le_pow_iff

added theorem one_le_pow_of_one_le'

added theorem one_le_zpow

added theorem one_lt_pow'

added theorem one_lt_pow_iff

added theorem pow_eq_one_iff

added theorem pow_le_one'

added theorem pow_le_one_iff

added theorem pow_le_pow'

added theorem pow_le_pow_iff'

added theorem pow_le_pow_of_le_left'

added theorem pow_le_pow_of_le_one'

added theorem pow_lt_one'

added theorem pow_lt_one_iff

added theorem pow_lt_pow'

added theorem pow_lt_pow_iff'

added theorem pow_mono_right

added theorem pow_strictMono_left

added theorem pow_strictMono_right'

Modified Mathlib/Algebra/GroupPower/Order.lean

deleted theorem Left.one_le_pow_of_le

deleted theorem Left.pow_le_one_of_le

deleted theorem Left.pow_lt_one_iff'

deleted theorem Left.pow_lt_one_iff

deleted theorem Left.pow_lt_one_of_lt

deleted theorem Monotone.pow_right

deleted theorem Right.one_le_pow_of_le

deleted theorem Right.pow_le_one_of_le

deleted theorem Right.pow_lt_one_iff

deleted theorem Right.pow_lt_one_of_lt

deleted theorem StrictMono.pow_right'

deleted theorem le_max_of_sq_le_mul

deleted theorem le_of_pow_le_pow'

deleted theorem lt_max_of_sq_lt_mul

deleted theorem lt_of_pow_lt_pow'

deleted theorem min_le_of_mul_le_sq

deleted theorem min_lt_of_mul_lt_sq

deleted theorem one_le_pow_iff

deleted theorem one_le_pow_of_one_le'

deleted theorem one_le_zpow

deleted theorem one_lt_pow'

deleted theorem one_lt_pow_iff

deleted theorem pow_eq_one_iff

deleted theorem pow_le_one'

deleted theorem pow_le_one_iff

deleted theorem pow_le_pow'

deleted theorem pow_le_pow_iff'

deleted theorem pow_le_pow_of_le_left'

deleted theorem pow_le_pow_of_le_one'

deleted theorem pow_lt_one'

deleted theorem pow_lt_one_iff

deleted theorem pow_lt_pow'

deleted theorem pow_lt_pow_iff'

deleted theorem pow_mono_right

deleted theorem pow_strictMono_left

deleted theorem pow_strictMono_right'