Constructing an ordered ring from a ring with a specified positive cone. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Positive cones #
Forget that a positive cone in a ring respects the multiplicative structure.
@[nolint]
- nonneg : α → Prop
- pos : α → Prop
- pos_iff : (∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)) . "order_laws_tac"
- zero_nonneg : self.nonneg 0
- add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
- nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0
- one_nonneg : self.nonneg 1
- mul_pos : ∀ (a b : α), self.pos a → self.pos b → self.pos (a * b)
A positive cone in a ring consists of a positive cone in underlying add_comm_group,
which contains 1 and such that the positive elements are closed under multiplication.
Instances for ring.positive_cone
- ring.positive_cone.has_sizeof_inst
@[nolint]
- nonneg : α → Prop
- pos : α → Prop
- pos_iff : (∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)) . "order_laws_tac"
- zero_nonneg : self.nonneg 0
- add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
- nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0
- one_nonneg : self.nonneg 1
- mul_pos : ∀ (a b : α), self.pos a → self.pos b → self.pos (a * b)
- nonneg_decidable : decidable_pred self.nonneg
- nonneg_total : ∀ (a : α), self.nonneg a ∨ self.nonneg (-a)
A total positive cone in a nontrivial ring induces a linear order.
Instances for ring.total_positive_cone
- ring.total_positive_cone.has_sizeof_inst
def
ring.total_positive_cone.to_total_positive_cone
{α : Type u_2}
[ring α]
(self : ring.total_positive_cone α) :
Forget that a total_positive_cone in a ring respects the multiplicative structure.
def
ring.total_positive_cone.to_positive_cone
{α : Type u_2}
[ring α]
(self : ring.total_positive_cone α) :
Forget that a total_positive_cone in a ring is total.
theorem
ring.positive_cone.one_pos
{α : Type u_1}
[ring α]
[nontrivial α]
(C : ring.positive_cone α) :
C.pos 1
def
strict_ordered_ring.mk_of_positive_cone
{α : Type u_1}
[ring α]
[nontrivial α]
(C : ring.positive_cone α) :
Construct a strict_ordered_ring by designating a positive cone in an existing ring.
Equations
- strict_ordered_ring.mk_of_positive_cone C = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_1, sub := ring.sub _inst_1, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast _inst_1, nat_cast := ring.nat_cast _inst_1, one := ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le (ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone), lt := ordered_add_comm_group.lt (ordered_add_comm_group.mk_of_positive_cone C.to_positive_cone), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _}
def
linear_ordered_ring.mk_of_positive_cone
{α : Type u_1}
[ring α]
[nontrivial α]
(C : ring.total_positive_cone α) :
Construct a linear_ordered_ring by
designating a positive cone in an existing ring.
Equations
- linear_ordered_ring.mk_of_positive_cone C = {add := strict_ordered_ring.add (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), add_assoc := _, zero := strict_ordered_ring.zero (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), sub := strict_ordered_ring.sub (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), nat_cast := strict_ordered_ring.nat_cast (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), one := strict_ordered_ring.one (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), lt := strict_ordered_ring.lt (strict_ordered_ring.mk_of_positive_cone C.to_positive_cone), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_add_comm_group.decidable_le (linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone), decidable_eq := linear_ordered_add_comm_group.decidable_eq (linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone), decidable_lt := linear_ordered_add_comm_group.decidable_lt (linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone), max := linear_ordered_add_comm_group.max (linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone), max_def := _, min := linear_ordered_add_comm_group.min (linear_ordered_add_comm_group.mk_of_positive_cone C.to_total_positive_cone), min_def := _}