Commit 2020-11-22 19:31 2a876b65

View on Github →

chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066) Replace one 2000 line file with two 1000 line files: ordered group stuff in one, and ordered monoid stuff in the other.

Estimated changes

Modified src/algebra/ordered_group.lean

deleted theorem add_eq_zero_iff

deleted theorem bit0_pos

deleted theorem bot_eq_zero

deleted theorem exists_pos_add_of_lt

deleted theorem fn_min_mul_fn_max

deleted theorem le_add_left

deleted theorem le_add_right

deleted theorem le_iff_exists_add

deleted theorem le_mul_iff_one_le_left'

deleted theorem le_mul_iff_one_le_right'

deleted theorem le_mul_of_le_of_one_le

deleted theorem le_mul_of_one_le_left'

deleted theorem le_mul_of_one_le_of_le

deleted theorem le_mul_of_one_le_right'

deleted theorem le_of_mul_le_mul_left'

deleted theorem le_of_mul_le_mul_right'

deleted theorem le_zero_iff_eq

deleted theorem lt_mul_iff_one_lt_left'

deleted theorem lt_mul_iff_one_lt_right'

deleted theorem lt_mul_of_le_of_one_lt

deleted theorem lt_mul_of_lt_of_one_le'

deleted theorem lt_mul_of_lt_of_one_le

deleted theorem lt_mul_of_lt_of_one_lt'

deleted theorem lt_mul_of_lt_of_one_lt

deleted theorem lt_mul_of_one_le_of_lt'

deleted theorem lt_mul_of_one_le_of_lt

deleted theorem lt_mul_of_one_lt_left'

deleted theorem lt_mul_of_one_lt_of_le

deleted theorem lt_mul_of_one_lt_of_lt'

deleted theorem lt_mul_of_one_lt_of_lt

deleted theorem lt_mul_of_one_lt_right'

deleted theorem lt_of_mul_lt_mul_left'

deleted theorem lt_of_mul_lt_mul_right'

deleted theorem max_add_add_left

deleted theorem max_add_add_right

deleted theorem max_le_add_of_nonneg

deleted theorem min_add_add_left

deleted theorem min_add_add_right

deleted theorem min_le_add_of_nonneg_left

deleted theorem min_le_add_of_nonneg_right

deleted theorem min_mul_max

deleted theorem monotone.const_mul'

deleted theorem monotone.mul'

deleted theorem monotone.mul_const'

deleted theorem monotone.mul_strict_mono'

deleted theorem mul_eq_one_iff'

deleted theorem mul_eq_one_iff_eq_one_of_one_le

deleted theorem mul_le_iff_le_one_left'

deleted theorem mul_le_iff_le_one_right'

deleted theorem mul_le_mul'

deleted theorem mul_le_mul_iff_left

deleted theorem mul_le_mul_iff_right

deleted theorem mul_le_mul_left'

deleted theorem mul_le_mul_right'

deleted theorem mul_le_mul_three

deleted theorem mul_le_of_le_of_le_one'

deleted theorem mul_le_of_le_of_le_one

deleted theorem mul_le_of_le_one_of_le'

deleted theorem mul_le_of_le_one_of_le

deleted theorem mul_le_one'

deleted theorem mul_lt_iff_lt_one_left'

deleted theorem mul_lt_iff_lt_one_right'

deleted theorem mul_lt_mul'''

deleted theorem mul_lt_mul_iff_left

deleted theorem mul_lt_mul_iff_right

deleted theorem mul_lt_mul_left'

deleted theorem mul_lt_mul_of_le_of_lt

deleted theorem mul_lt_mul_of_lt_of_le

deleted theorem mul_lt_mul_right'

deleted theorem mul_lt_of_le_of_lt_one

deleted theorem mul_lt_of_le_one_of_lt'

deleted theorem mul_lt_of_le_one_of_lt

deleted theorem mul_lt_of_lt_of_le_one'

deleted theorem mul_lt_of_lt_of_le_one

deleted theorem mul_lt_of_lt_of_lt_one'

deleted theorem mul_lt_of_lt_of_lt_one

deleted theorem mul_lt_of_lt_one_of_le

deleted theorem mul_lt_of_lt_one_of_lt'

deleted theorem mul_lt_of_lt_one_of_lt

deleted theorem mul_lt_one'

deleted theorem mul_lt_one

deleted theorem mul_lt_one_of_le_one_of_lt_one'

deleted theorem mul_lt_one_of_le_one_of_lt_one

deleted theorem mul_lt_one_of_lt_one_of_le_one'

deleted theorem mul_lt_one_of_lt_one_of_le_one

deleted theorem one_le_mul

deleted theorem one_lt_mul'

deleted theorem one_lt_mul_of_le_of_lt'

deleted theorem one_lt_mul_of_lt_of_le'

deleted theorem strict_mono.const_mul'

deleted theorem strict_mono.mul_const'

deleted theorem strict_mono.mul_monotone'

deleted theorem units.coe_le_coe

deleted theorem units.coe_lt_coe

deleted theorem units.max_coe

deleted theorem units.min_coe

deleted theorem with_bot.add_bot

deleted theorem with_bot.add_lt_add_iff_left

deleted theorem with_bot.add_lt_add_iff_right

deleted theorem with_bot.bot_add

deleted theorem with_bot.coe_add

deleted theorem with_bot.coe_bit0

deleted theorem with_bot.coe_bit1

deleted theorem with_bot.coe_eq_zero

deleted theorem with_bot.coe_one

deleted theorem with_bot.coe_zero

deleted theorem with_top.add_eq_coe

deleted theorem with_top.add_eq_top

deleted theorem with_top.add_lt_add_iff_left

deleted theorem with_top.add_lt_add_iff_right

deleted theorem with_top.add_lt_top

deleted theorem with_top.add_top

deleted theorem with_top.coe_add

deleted def with_top.coe_add_hom

deleted theorem with_top.coe_bit0

deleted theorem with_top.coe_bit1

deleted theorem with_top.coe_coe_add_hom

deleted theorem with_top.coe_eq_one

deleted theorem with_top.coe_one

deleted theorem with_top.one_eq_coe

deleted theorem with_top.one_ne_top

deleted theorem with_top.top_add

deleted theorem with_top.top_ne_one

deleted theorem with_top.zero_lt_coe

deleted theorem with_top.zero_lt_top

deleted theorem with_zero.coe_le_coe

deleted theorem with_zero.coe_lt_coe

deleted theorem with_zero.lt_of_mul_lt_mul_left

deleted theorem with_zero.mul_le_mul_left

deleted def with_zero.ordered_add_comm_monoid

deleted theorem with_zero.zero_le

deleted theorem with_zero.zero_lt_coe

deleted theorem zero_le

deleted theorem zero_lt_iff_ne_zero

Created src/algebra/ordered_monoid.lean

added theorem add_eq_zero_iff

added theorem bit0_pos

added theorem bot_eq_zero

added theorem exists_pos_add_of_lt

added theorem fn_min_mul_fn_max

added theorem le_add_left

added theorem le_add_right

added theorem le_iff_exists_add

added theorem le_mul_iff_one_le_left'

added theorem le_mul_iff_one_le_right'

added theorem le_mul_of_le_of_one_le

added theorem le_mul_of_one_le_left'

added theorem le_mul_of_one_le_of_le

added theorem le_mul_of_one_le_right'

added theorem le_of_mul_le_mul_left'

added theorem le_of_mul_le_mul_right'

added theorem le_zero_iff_eq

added theorem lt_mul_iff_one_lt_left'

added theorem lt_mul_iff_one_lt_right'

added theorem lt_mul_of_le_of_one_lt

added theorem lt_mul_of_lt_of_one_le'

added theorem lt_mul_of_lt_of_one_le

added theorem lt_mul_of_lt_of_one_lt'

added theorem lt_mul_of_lt_of_one_lt

added theorem lt_mul_of_one_le_of_lt'

added theorem lt_mul_of_one_le_of_lt

added theorem lt_mul_of_one_lt_left'

added theorem lt_mul_of_one_lt_of_le

added theorem lt_mul_of_one_lt_of_lt'

added theorem lt_mul_of_one_lt_of_lt

added theorem lt_mul_of_one_lt_right'

added theorem lt_of_mul_lt_mul_left'

added theorem lt_of_mul_lt_mul_right'

added theorem max_add_add_left

added theorem max_add_add_right

added theorem max_le_add_of_nonneg

added theorem min_add_add_left

added theorem min_add_add_right

added theorem min_le_add_of_nonneg_left

added theorem min_le_add_of_nonneg_right

added theorem min_mul_max

added theorem monotone.const_mul'

added theorem monotone.mul'

added theorem monotone.mul_const'

added theorem monotone.mul_strict_mono'

added theorem mul_eq_one_iff'

added theorem mul_eq_one_iff_eq_one_of_one_le

added theorem mul_le_iff_le_one_left'

added theorem mul_le_iff_le_one_right'

added theorem mul_le_mul'

added theorem mul_le_mul_iff_left

added theorem mul_le_mul_iff_right

added theorem mul_le_mul_left'

added theorem mul_le_mul_right'

added theorem mul_le_mul_three

added theorem mul_le_of_le_of_le_one'

added theorem mul_le_of_le_of_le_one

added theorem mul_le_of_le_one_of_le'

added theorem mul_le_of_le_one_of_le

added theorem mul_le_one'

added theorem mul_lt_iff_lt_one_left'

added theorem mul_lt_iff_lt_one_right'

added theorem mul_lt_mul'''

added theorem mul_lt_mul_iff_left

added theorem mul_lt_mul_iff_right

added theorem mul_lt_mul_left'

added theorem mul_lt_mul_of_le_of_lt

added theorem mul_lt_mul_of_lt_of_le

added theorem mul_lt_mul_right'

added theorem mul_lt_of_le_of_lt_one

added theorem mul_lt_of_le_one_of_lt'

added theorem mul_lt_of_le_one_of_lt

added theorem mul_lt_of_lt_of_le_one'

added theorem mul_lt_of_lt_of_le_one

added theorem mul_lt_of_lt_of_lt_one'

added theorem mul_lt_of_lt_of_lt_one

added theorem mul_lt_of_lt_one_of_le

added theorem mul_lt_of_lt_one_of_lt'

added theorem mul_lt_of_lt_one_of_lt

added theorem mul_lt_one'

added theorem mul_lt_one

added theorem mul_lt_one_of_le_one_of_lt_one'

added theorem mul_lt_one_of_le_one_of_lt_one

added theorem mul_lt_one_of_lt_one_of_le_one'

added theorem mul_lt_one_of_lt_one_of_le_one

added theorem one_le_mul

added theorem one_lt_mul'

added theorem one_lt_mul_of_le_of_lt'

added theorem one_lt_mul_of_lt_of_le'

added theorem strict_mono.const_mul'

added theorem strict_mono.mul_const'

added theorem strict_mono.mul_monotone'

added theorem units.coe_le_coe

added theorem units.coe_lt_coe

added theorem units.max_coe

added theorem units.min_coe

added theorem with_bot.add_bot

added theorem with_bot.add_lt_add_iff_left

added theorem with_bot.add_lt_add_iff_right

added theorem with_bot.bot_add

added theorem with_bot.coe_add

added theorem with_bot.coe_bit0

added theorem with_bot.coe_bit1

added theorem with_bot.coe_eq_zero

added theorem with_bot.coe_one

added theorem with_bot.coe_zero

added theorem with_top.add_eq_coe

added theorem with_top.add_eq_top

added theorem with_top.add_lt_add_iff_left

added theorem with_top.add_lt_add_iff_right

added theorem with_top.add_lt_top

added theorem with_top.add_top

added theorem with_top.coe_add

added def with_top.coe_add_hom

added theorem with_top.coe_bit0

added theorem with_top.coe_bit1

added theorem with_top.coe_coe_add_hom

added theorem with_top.coe_eq_one

added theorem with_top.coe_one

added theorem with_top.one_eq_coe

added theorem with_top.one_ne_top

added theorem with_top.top_add

added theorem with_top.top_ne_one

added theorem with_top.zero_lt_coe

added theorem with_top.zero_lt_top

added theorem with_zero.coe_le_coe

added theorem with_zero.coe_lt_coe

added theorem with_zero.lt_of_mul_lt_mul_left

added theorem with_zero.mul_le_mul_left

added def with_zero.ordered_add_comm_monoid

added theorem with_zero.zero_le

added theorem with_zero.zero_lt_coe

added theorem zero_le

added theorem zero_lt_iff_ne_zero