mathlib3 documentation

algebra.order.ring.cone

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]
structure ring.positive_cone (α : Type u_2) [ring α] :
Type u_2

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]
structure ring.total_positive_cone (α : Type u_2) [ring α] :
Type u_2

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

Forget that a total_positive_cone in a ring respects the multiplicative structure.

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

Construct a linear_ordered_ring by designating a positive cone in an existing ring.

Equations