English
For n ≠ 0, the additive submonoid generated by nth powers of nonnegative rationals is the whole nonnegative rationals: closure({ x^n : x ≥ 0, x ∈ ℚ }) = ⊤.
Русский
Для n ≠ 0 множество порожденных степенями n-нных нечётких рациональных неотрицательных чисел образует всю неотрицательную часть ℚ.
LaTeX
$$$ \operatorname{closure}(\{ x^n : x \in \mathbb{Q}_{\ge 0} \}) = \top, \quad n \neq 0 $$$
Lean4
@[simp]
theorem addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) : closure (range fun x : ℚ≥0 ↦ x ^ n) = ⊤ :=
by
refine (eq_top_iff' _).2 fun x ↦ ?_
suffices x = (x.num * x.den ^ (n - 1)) • (x.den : ℚ≥0)⁻¹ ^ n
by
rw [this]
exact nsmul_mem (subset_closure <| mem_range_self _) _
rw [nsmul_eq_mul]
push_cast
rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul, ← div_eq_mul_inv,
num_div_den]
all_goals simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]
