Commit 2024-07-07 14:44 70e5cb98

View on Github →

chore (Algebra.Order.Group.Defs): split out unbundled ordered algebra results to Algebra.Order.Group.Unbundled.Basic (#14380) Currently, you have to import bundled ordered algebra to use these facts about unbundled ordered algebra classes. This should be unnecessary.

Estimated changes

deleted theorem Antitone.inv
deleted theorem AntitoneOn.inv
deleted theorem Left.inv_le_one_iff
deleted theorem Left.inv_le_self
deleted theorem Left.inv_lt_one_iff
deleted theorem Left.inv_lt_self
deleted theorem Left.one_le_inv_iff
deleted theorem Left.one_lt_inv_iff
deleted theorem Left.self_le_inv
deleted theorem Left.self_lt_inv
deleted theorem Monotone.inv
deleted theorem MonotoneOn.inv
deleted theorem Right.inv_le_one_iff
deleted theorem Right.inv_le_self
deleted theorem Right.inv_lt_one_iff
deleted theorem Right.inv_lt_self
deleted theorem Right.one_le_inv_iff
deleted theorem Right.one_lt_inv_iff
deleted theorem Right.self_le_inv
deleted theorem Right.self_lt_inv
deleted theorem StrictAnti.inv
deleted theorem StrictAntiOn.inv
deleted theorem StrictMono.inv
deleted theorem StrictMonoOn.inv
deleted theorem cmp_div_one'
deleted theorem div_le_comm
deleted theorem div_le_div''
deleted theorem div_le_div_flip
deleted theorem div_le_div_iff'
deleted theorem div_le_div_iff_left
deleted theorem div_le_div_iff_right
deleted theorem div_le_div_left'
deleted theorem div_le_div_right'
deleted theorem div_le_iff_le_mul'
deleted theorem div_le_iff_le_mul
deleted theorem div_le_inv_mul_iff
deleted theorem div_le_one'
deleted theorem div_le_self_iff
deleted theorem div_lt_comm
deleted theorem div_lt_div''
deleted theorem div_lt_div_iff'
deleted theorem div_lt_div_iff_left
deleted theorem div_lt_div_iff_right
deleted theorem div_lt_div_left'
deleted theorem div_lt_div_right'
deleted theorem div_lt_iff_lt_mul'
deleted theorem div_lt_iff_lt_mul
deleted theorem div_lt_one'
deleted theorem div_lt_self_iff
deleted theorem inv_le_div_iff_le_mul'
deleted theorem inv_le_div_iff_le_mul
deleted theorem inv_le_iff_one_le_mul'
deleted theorem inv_le_iff_one_le_mul
deleted theorem inv_le_inv_iff
deleted theorem inv_lt'
deleted theorem inv_lt_div_iff_lt_mul'
deleted theorem inv_lt_div_iff_lt_mul
deleted theorem inv_lt_iff_one_lt_mul'
deleted theorem inv_lt_iff_one_lt_mul
deleted theorem inv_lt_inv_iff
deleted theorem inv_mul_le_iff_le_mul'
deleted theorem inv_mul_le_iff_le_mul
deleted theorem inv_mul_le_one_iff
deleted theorem inv_mul_lt_iff_lt_mul'
deleted theorem inv_mul_lt_iff_lt_mul
deleted theorem inv_mul_lt_one_iff
deleted theorem inv_mul_lt_one_iff_lt
deleted theorem le_div_comm
deleted theorem le_div_iff_mul_le'
deleted theorem le_div_iff_mul_le
deleted theorem le_div_self_iff
deleted theorem le_inv_mul_iff_le
deleted theorem le_inv_mul_iff_mul_le
deleted theorem le_mul_inv_iff_le
deleted theorem le_mul_inv_iff_mul_le
deleted theorem lt_div_comm
deleted theorem lt_div_iff_mul_lt'
deleted theorem lt_div_iff_mul_lt
deleted theorem lt_inv'
deleted theorem lt_inv_iff_mul_lt_one'
deleted theorem lt_inv_iff_mul_lt_one
deleted theorem lt_inv_mul_iff_lt
deleted theorem lt_inv_mul_iff_mul_lt
deleted theorem lt_mul_inv_iff_lt
deleted theorem lt_mul_inv_iff_mul_lt
deleted theorem lt_or_lt_of_div_lt_div
deleted theorem mul_inv_le_iff_le_mul'
deleted theorem mul_inv_le_iff_le_mul
deleted theorem mul_inv_le_inv_mul_iff
deleted theorem mul_inv_le_mul_inv_iff'
deleted theorem mul_inv_le_one_iff
deleted theorem mul_inv_le_one_iff_le
deleted theorem mul_inv_lt_iff_le_mul'
deleted theorem mul_inv_lt_iff_lt_mul
deleted theorem mul_inv_lt_inv_mul_iff
deleted theorem mul_inv_lt_mul_inv_iff'
deleted theorem mul_inv_lt_one_iff
deleted theorem one_le_div'
deleted theorem one_lt_div'
added theorem Antitone.inv
added theorem AntitoneOn.inv
added theorem Left.inv_le_one_iff
added theorem Left.inv_le_self
added theorem Left.inv_lt_one_iff
added theorem Left.inv_lt_self
added theorem Left.one_le_inv_iff
added theorem Left.one_lt_inv_iff
added theorem Left.self_le_inv
added theorem Left.self_lt_inv
added theorem Monotone.inv
added theorem MonotoneOn.inv
added theorem Right.inv_le_one_iff
added theorem Right.inv_le_self
added theorem Right.inv_lt_one_iff
added theorem Right.inv_lt_self
added theorem Right.one_le_inv_iff
added theorem Right.one_lt_inv_iff
added theorem Right.self_le_inv
added theorem Right.self_lt_inv
added theorem StrictAnti.inv
added theorem StrictAntiOn.inv
added theorem StrictMono.inv
added theorem StrictMonoOn.inv
added theorem cmp_div_one'
added theorem div_le_comm
added theorem div_le_div''
added theorem div_le_div_flip
added theorem div_le_div_iff'
added theorem div_le_div_iff_left
added theorem div_le_div_iff_right
added theorem div_le_div_left'
added theorem div_le_div_right'
added theorem div_le_iff_le_mul'
added theorem div_le_iff_le_mul
added theorem div_le_inv_mul_iff
added theorem div_le_one'
added theorem div_le_self_iff
added theorem div_lt_comm
added theorem div_lt_div''
added theorem div_lt_div_iff'
added theorem div_lt_div_iff_left
added theorem div_lt_div_iff_right
added theorem div_lt_div_left'
added theorem div_lt_div_right'
added theorem div_lt_iff_lt_mul'
added theorem div_lt_iff_lt_mul
added theorem div_lt_one'
added theorem div_lt_self_iff
added theorem inv_le_div_iff_le_mul'
added theorem inv_le_div_iff_le_mul
added theorem inv_le_iff_one_le_mul'
added theorem inv_le_iff_one_le_mul
added theorem inv_le_inv_iff
added theorem inv_lt'
added theorem inv_lt_div_iff_lt_mul'
added theorem inv_lt_div_iff_lt_mul
added theorem inv_lt_iff_one_lt_mul'
added theorem inv_lt_iff_one_lt_mul
added theorem inv_lt_inv_iff
added theorem inv_mul_le_iff_le_mul'
added theorem inv_mul_le_iff_le_mul
added theorem inv_mul_le_one_iff
added theorem inv_mul_lt_iff_lt_mul'
added theorem inv_mul_lt_iff_lt_mul
added theorem inv_mul_lt_one_iff
added theorem inv_mul_lt_one_iff_lt
added theorem le_div_comm
added theorem le_div_iff_mul_le'
added theorem le_div_iff_mul_le
added theorem le_div_self_iff
added theorem le_inv_mul_iff_le
added theorem le_inv_mul_iff_mul_le
added theorem le_mul_inv_iff_le
added theorem le_mul_inv_iff_mul_le
added theorem lt_div_comm
added theorem lt_div_iff_mul_lt'
added theorem lt_div_iff_mul_lt
added theorem lt_inv'
added theorem lt_inv_iff_mul_lt_one'
added theorem lt_inv_iff_mul_lt_one
added theorem lt_inv_mul_iff_lt
added theorem lt_inv_mul_iff_mul_lt
added theorem lt_mul_inv_iff_lt
added theorem lt_mul_inv_iff_mul_lt
added theorem lt_or_lt_of_div_lt_div
added theorem mul_inv_le_iff_le_mul'
added theorem mul_inv_le_iff_le_mul
added theorem mul_inv_le_inv_mul_iff
added theorem mul_inv_le_one_iff
added theorem mul_inv_le_one_iff_le
added theorem mul_inv_lt_iff_le_mul'
added theorem mul_inv_lt_iff_lt_mul
added theorem mul_inv_lt_inv_mul_iff
added theorem mul_inv_lt_one_iff
added theorem one_le_div'
added theorem one_lt_div'