Commit 2022-10-09 22:10 8ef4f3fa

View on Github →

chore(algebra/order/monoid): split into smaller files (#16861) This, along later PRs for algebra.order.group and algebra.order.ring, will replace #16792.

depends on: #16172

Estimated changes

Modified counterexamples/canonically_ordered_comm_semiring_two_mul.lean

Modified counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean

Modified src/algebra/order/group.lean

Deleted src/algebra/order/monoid.lean

deleted theorem add_top

deleted theorem additive.of_mul_le

deleted theorem additive.of_mul_lt

deleted theorem additive.to_mul_le

deleted theorem additive.to_mul_lt

deleted theorem bit0_pos

deleted theorem bot_eq_one'

deleted theorem bot_eq_one

deleted theorem eq_one_or_one_lt

deleted theorem exists_one_lt_mul_of_lt

deleted theorem fn_min_mul_fn_max

deleted def function.injective.linear_ordered_cancel_comm_monoid

deleted def function.injective.linear_ordered_comm_monoid

deleted def function.injective.ordered_cancel_comm_monoid

deleted def function.injective.ordered_comm_monoid

deleted theorem has_mul.to_covariant_class_left

deleted theorem has_mul.to_covariant_class_right

deleted theorem le_iff_exists_mul'

deleted theorem le_iff_exists_mul

deleted theorem le_iff_forall_one_lt_lt_mul'

deleted theorem le_mul_left

deleted theorem le_mul_right

deleted theorem le_mul_self

deleted theorem le_of_forall_one_lt_le_mul

deleted theorem le_of_forall_one_lt_lt_mul'

deleted theorem le_of_mul_le_left

deleted theorem le_of_mul_le_right

deleted theorem le_one_iff_eq_one

deleted theorem le_self_mul

deleted theorem lt_iff_exists_mul

deleted theorem lt_or_lt_of_mul_lt_mul

deleted theorem max_le_mul_of_one_le

deleted theorem max_mul_mul_left

deleted theorem max_mul_mul_right

deleted theorem min_le_mul_of_one_le_left

deleted theorem min_le_mul_of_one_le_right

deleted theorem min_mul_distrib'

deleted theorem min_mul_distrib

deleted theorem min_mul_max

deleted theorem min_mul_mul_left

deleted theorem min_mul_mul_right

deleted theorem min_one

deleted theorem mul_eq_one_iff

deleted theorem mul_lt_mul_iff_of_le_of_le

deleted theorem multiplicative.of_add_le

deleted theorem multiplicative.of_add_lt

deleted theorem multiplicative.to_add_le

deleted theorem multiplicative.to_add_lt

deleted theorem one_le

deleted theorem one_le_two'

deleted theorem one_le_two

deleted theorem one_lt_iff_ne_one

deleted theorem one_lt_mul_iff

deleted theorem one_min

deleted def order_embedding.mul_left

deleted def order_embedding.mul_right

deleted theorem ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left

deleted theorem pos_of_gt

deleted theorem self_le_mul_left

deleted theorem self_le_mul_right

deleted theorem top_add

deleted theorem units.coe_le_coe

deleted theorem units.coe_lt_coe

deleted theorem units.max_coe

deleted theorem units.min_coe

deleted def units.order_embedding_coe

deleted theorem with_bot.add_bot

deleted theorem with_bot.add_coe_eq_bot_iff

deleted theorem with_bot.add_eq_bot

deleted theorem with_bot.add_eq_coe

deleted theorem with_bot.add_ne_bot

deleted theorem with_bot.bot_add

deleted theorem with_bot.bot_lt_add

deleted theorem with_bot.bot_ne_nat

deleted theorem with_bot.coe_add

deleted theorem with_bot.coe_add_eq_bot_iff

deleted theorem with_bot.coe_bit0

deleted theorem with_bot.coe_bit1

deleted theorem with_bot.coe_eq_one

deleted theorem with_bot.coe_nat

deleted theorem with_bot.coe_one

deleted theorem with_bot.nat_ne_bot

deleted theorem with_top.add_coe_eq_top_iff

deleted theorem with_top.add_eq_coe

deleted theorem with_top.add_eq_top

deleted theorem with_top.add_lt_top

deleted theorem with_top.add_ne_top

deleted theorem with_top.add_top

deleted theorem with_top.coe_add

deleted theorem with_top.coe_add_eq_top_iff

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_nat

deleted theorem with_top.coe_one

deleted theorem with_top.nat_ne_top

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_nat

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.le_max_iff

deleted theorem with_zero.min_le_iff

deleted def with_zero.to_mul_bot

deleted theorem with_zero.to_mul_bot_coe

deleted theorem with_zero.to_mul_bot_coe_of_add

deleted theorem with_zero.to_mul_bot_le

deleted theorem with_zero.to_mul_bot_lt

deleted theorem with_zero.to_mul_bot_strict_mono

deleted theorem with_zero.to_mul_bot_symm_bot

deleted theorem with_zero.to_mul_bot_zero

deleted theorem with_zero.zero_eq_bot

deleted theorem with_zero.zero_le

deleted theorem with_zero.zero_lt_coe

deleted theorem zero_le_four

deleted theorem zero_le_one'

deleted theorem zero_le_one

deleted theorem zero_le_three

deleted theorem zero_le_two

Created src/algebra/order/monoid/basic.lean

added theorem add_top

added theorem bit0_pos

added def function.injective.linear_ordered_comm_monoid

added def function.injective.ordered_comm_monoid

added theorem has_mul.to_covariant_class_left

added theorem has_mul.to_covariant_class_right

added def order_embedding.mul_left

added def order_embedding.mul_right

added theorem top_add

Created src/algebra/order/monoid/cancel.lean

added def function.injective.linear_ordered_cancel_comm_monoid

added def function.injective.ordered_cancel_comm_monoid

added theorem ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left

Created src/algebra/order/monoid/canonical.lean

added theorem bot_eq_one'

added theorem bot_eq_one

added theorem eq_one_or_one_lt

added theorem exists_one_lt_mul_of_lt

added theorem le_iff_exists_mul'

added theorem le_iff_exists_mul

added theorem le_iff_forall_one_lt_lt_mul'

added theorem le_mul_left

added theorem le_mul_right

added theorem le_mul_self

added theorem le_of_forall_one_lt_le_mul

added theorem le_of_forall_one_lt_lt_mul'

added theorem le_of_mul_le_left

added theorem le_of_mul_le_right

added theorem le_one_iff_eq_one

added theorem le_self_mul

added theorem lt_iff_exists_mul

added theorem min_mul_distrib'

added theorem min_mul_distrib

added theorem min_one

added theorem mul_eq_one_iff

added theorem one_le

added theorem one_lt_iff_ne_one

added theorem one_lt_mul_iff

added theorem one_min

added theorem pos_of_gt

added theorem self_le_mul_left

added theorem self_le_mul_right

Renamed src/algebra/order/monoid_lemmas.lean to src/algebra/order/monoid/lemmas.lean

Created src/algebra/order/monoid/min_max.lean

added theorem fn_min_mul_fn_max

added theorem lt_or_lt_of_mul_lt_mul

added theorem max_le_mul_of_one_le

added theorem max_mul_mul_left

added theorem max_mul_mul_right

added theorem min_le_mul_of_one_le_left

added theorem min_le_mul_of_one_le_right

added theorem min_mul_max

added theorem min_mul_mul_left

added theorem min_mul_mul_right

added theorem mul_lt_mul_iff_of_le_of_le

Created src/algebra/order/monoid/order_dual.lean

Created src/algebra/order/monoid/prod.lean

Created src/algebra/order/monoid/to_mul_bot.lean

added def with_zero.to_mul_bot

added theorem with_zero.to_mul_bot_coe

added theorem with_zero.to_mul_bot_coe_of_add

added theorem with_zero.to_mul_bot_le

added theorem with_zero.to_mul_bot_lt

added theorem with_zero.to_mul_bot_strict_mono

added theorem with_zero.to_mul_bot_symm_bot

added theorem with_zero.to_mul_bot_zero

Created src/algebra/order/monoid/type_tags.lean

added theorem additive.of_mul_le

added theorem additive.of_mul_lt

added theorem additive.to_mul_le

added theorem additive.to_mul_lt

added theorem multiplicative.of_add_le

added theorem multiplicative.of_add_lt

added theorem multiplicative.to_add_le

added theorem multiplicative.to_add_lt

Created src/algebra/order/monoid/units.lean

added theorem units.coe_le_coe

added theorem units.coe_lt_coe

added theorem units.max_coe

added theorem units.min_coe

added def units.order_embedding_coe

Created src/algebra/order/monoid/with_top.lean

added theorem with_bot.add_bot

added theorem with_bot.add_coe_eq_bot_iff

added theorem with_bot.add_eq_bot

added theorem with_bot.add_eq_coe

added theorem with_bot.add_ne_bot

added theorem with_bot.bot_add

added theorem with_bot.bot_lt_add

added theorem with_bot.bot_ne_nat

added theorem with_bot.coe_add

added theorem with_bot.coe_add_eq_bot_iff

added theorem with_bot.coe_bit0

added theorem with_bot.coe_bit1

added theorem with_bot.coe_eq_one

added theorem with_bot.coe_nat

added theorem with_bot.coe_one

added theorem with_bot.nat_ne_bot

added theorem with_top.add_coe_eq_top_iff

added theorem with_top.add_eq_coe

added theorem with_top.add_eq_top

added theorem with_top.add_lt_top

added theorem with_top.add_ne_top

added theorem with_top.add_top

added theorem with_top.coe_add

added theorem with_top.coe_add_eq_top_iff

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_nat

added theorem with_top.coe_one

added theorem with_top.nat_ne_top

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_nat

added theorem with_top.top_ne_one

added theorem with_top.zero_lt_coe

added theorem with_top.zero_lt_top

Created src/algebra/order/monoid/with_zero.lean

added theorem with_zero.coe_le_coe

added theorem with_zero.coe_lt_coe

added theorem with_zero.le_max_iff

added theorem with_zero.min_le_iff

added theorem with_zero.zero_eq_bot

added theorem with_zero.zero_le

added theorem with_zero.zero_lt_coe

Modified src/algebra/order/sub.lean

Modified src/algebra/order/with_zero.lean

Created src/algebra/order/zero_le_one.lean

added theorem one_le_two'

added theorem one_le_two

added theorem zero_le_four

added theorem zero_le_one'

added theorem zero_le_one

added theorem zero_le_three

added theorem zero_le_two

Modified src/algebra/regular/basic.lean