Star ordered ring structure on ℤ

This file shows that ℤ is a StarOrderedRing.

@[simp]

theorem Int.addSubmonoid_closure_range_pow {n : ℕ} (hn : Even n) : AddSubmonoid.closure (Set.range fun (x : ℤ) => x ^ n) = AddSubmonoid.nonneg ℤ

@[simp]

theorem Int.addSubmonoid_closure_range_mul_self : AddSubmonoid.closure (Set.range fun (x : ℤ) => x * x) = AddSubmonoid.nonneg ℤ

instance Int.instStarOrderedRing : StarOrderedRing ℤ

Equations

• Int.instStarOrderedRing = ⋯