Strictly ordered field structure on π #
This file defines the following structures on π.
@[protected]
Equations
- is_R_or_C.partial_order = {le := Ξ» (z w : π), βis_R_or_C.re z β€ βis_R_or_C.re w β§ βis_R_or_C.im z = βis_R_or_C.im w, lt := Ξ» (z w : π), βis_R_or_C.re z < βis_R_or_C.re w β§ βis_R_or_C.im z = βis_R_or_C.im w, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
theorem
is_R_or_C.le_def
{π : Type u_1}
[is_R_or_C π]
{z w : π} :
z β€ w β βis_R_or_C.re z β€ βis_R_or_C.re w β§ βis_R_or_C.im z = βis_R_or_C.im w
theorem
is_R_or_C.lt_def
{π : Type u_1}
[is_R_or_C π]
{z w : π} :
z < w β βis_R_or_C.re z < βis_R_or_C.re w β§ βis_R_or_C.im z = βis_R_or_C.im w
theorem
is_R_or_C.nonneg_def
{π : Type u_1}
[is_R_or_C π]
{x : π} :
0 β€ x β 0 β€ βis_R_or_C.re x β§ βis_R_or_C.im x = 0
theorem
is_R_or_C.pos_def
{π : Type u_1}
[is_R_or_C π]
{x : π} :
0 < x β 0 < βis_R_or_C.re x β§ βis_R_or_C.im x = 0
theorem
is_R_or_C.nonpos_def
{π : Type u_1}
[is_R_or_C π]
{x : π} :
x β€ 0 β βis_R_or_C.re x β€ 0 β§ βis_R_or_C.im x = 0
theorem
is_R_or_C.neg_def
{π : Type u_1}
[is_R_or_C π]
{x : π} :
x < 0 β βis_R_or_C.re x < 0 β§ βis_R_or_C.im x = 0
theorem
is_R_or_C.nonneg_def'
{π : Type u_1}
[is_R_or_C π]
{x : π} :
0 β€ x β β(βis_R_or_C.re x) = x β§ 0 β€ βis_R_or_C.re x
theorem
is_R_or_C.not_le_iff
{π : Type u_1}
[is_R_or_C π]
{z w : π} :
Β¬z β€ w β βis_R_or_C.re w < βis_R_or_C.re z β¨ βis_R_or_C.im z β βis_R_or_C.im w
theorem
is_R_or_C.not_lt_iff
{π : Type u_1}
[is_R_or_C π]
{z w : π} :
Β¬z < w β βis_R_or_C.re w β€ βis_R_or_C.re z β¨ βis_R_or_C.im z β βis_R_or_C.im w
theorem
is_R_or_C.not_le_zero_iff
{π : Type u_1}
[is_R_or_C π]
{z : π} :
Β¬z β€ 0 β 0 < βis_R_or_C.re z β¨ βis_R_or_C.im z β 0
theorem
is_R_or_C.not_lt_zero_iff
{π : Type u_1}
[is_R_or_C π]
{z : π} :
Β¬z < 0 β 0 β€ βis_R_or_C.re z β¨ βis_R_or_C.im z β 0
@[protected]
With z β€ w iff w - z is real and nonnegative, π is a strictly ordered ring.
Equations
- is_R_or_C.strict_ordered_comm_ring = {add := comm_ring.add (field.to_comm_ring π), add_assoc := _, zero := comm_ring.zero (field.to_comm_ring π), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (field.to_comm_ring π), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (field.to_comm_ring π), sub := comm_ring.sub (field.to_comm_ring π), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (field.to_comm_ring π), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast (field.to_comm_ring π), nat_cast := comm_ring.nat_cast (field.to_comm_ring π), one := comm_ring.one (field.to_comm_ring π), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul (field.to_comm_ring π), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow (field.to_comm_ring π), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := partial_order.le is_R_or_C.partial_order, lt := partial_order.lt is_R_or_C.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, mul_comm := _}
@[protected]
With z β€ w iff w - z is real and nonnegative, π is a star ordered ring.
(That is, a star ring in which the nonnegative elements are those of the form star z * z.)
Equations
- is_R_or_C.star_ordered_ring = star_ordered_ring.of_nonneg_iff' is_R_or_C.star_ordered_ring._proof_1 is_R_or_C.star_ordered_ring._proof_2