pi.star_ordered_ring #
This file contains the definition of pi.star_ordered_ring.
theorem
add_submonoid.mem_pi
{ι : Type u_1}
[B : ι → Type u_2]
[Π (i : ι), add_zero_class (B i)]
(x : Π (i : ι), add_submonoid (B i))
(y : Π (i : ι), B i) :
theorem
set.pi_of_pi
{ι : Type u_1}
{B : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), add_zero_class (B i)]
{s : Π (i : ι), set (B i)}
(h : ∀ (i : ι), s i 0) :
def
add_submonoid.of_pi
{ι : Type u_1}
{B : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), add_zero_class (B i)] :
add_submonoid (Π (i : ι), B i) → Π (i : ι), add_submonoid (B i)
theorem
add_submonoid.pi_of_pi
{ι : Type u_1}
{B : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), add_zero_class (B i)]
(h : Π (i : ι), add_submonoid (B i)) :
(add_submonoid.pi set.univ h).of_pi = h
theorem
add_submonoid.closure_pi
{ι : Type u_1}
{B : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), add_zero_class (B i)]
{s : Π (i : ι), set (B i)}
{x : Π (i : ι), B i} :
x ∈ add_submonoid.closure (set.univ.pi (λ (i : ι), s i)) → ∀ (i : ι), x i ∈ add_submonoid.closure (s i)
theorem
pi.star_ordered_ring.nonneg_def
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), non_unital_semiring (α i)]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), star_ordered_ring (α i)]
(h : ∀ (i : ι) (x : α i), 0 ≤ x ↔ ∃ (y : α i), has_star.star y * y = x)
(x : Π (i : ι), α i) :
theorem
pi.star_ordered_ring.le_def
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), ring (α i)]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), star_ordered_ring (α i)]
(h : ∀ (i : ι) (x : α i), 0 ≤ x ↔ ∃ (y : α i), has_star.star y * y = x)
(x y : Π (i : ι), α i) :
def
pi.star_ordered_ring
{ι : Type u_1}
{B : ι → Type u_2}
[Π (i : ι), ring (B i)]
[Π (i : ι), partial_order (B i)]
[Π (i : ι), star_ordered_ring (B i)]
(h : ∀ (i : ι) (x : B i), 0 ≤ x ↔ ∃ (y : B i), has_star.star y * y = x) :
star_ordered_ring (Π (i : ι), B i)
Equations
- pi.star_ordered_ring h = star_ordered_ring.of_le_iff pi.star_ordered_ring._proof_1 _