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 ℤ