English
Let n ∈ ℕ with n ≠ 0 and n even. The closure of the set { x^n : x ∈ ℚ } in the rationals equals the nonnegative rationals.
Русский
Пусть n — натуральное не ноль и чётное. Замыкание множества { x^n : x ∈ ℚ } в рациональных числах даёт все неотрицательные рациональные числа.
LaTeX
$$$ \operatorname{closure}(\{ x^n : x \in \mathbb{Q} \}) = \operatorname{nonneg}(\mathbb{Q}) \quad (n \text{ even}, \ n \neq 0) $$$
Lean4
@[simp]
theorem addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) :
closure (range fun x : ℚ ↦ x ^ n) = nonneg _ :=
by
convert (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm
· have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩
simp [subset_antisymm_iff, range_subset_iff, this]
· ext
simp [NNRat.addSubmonoid_closure_range_pow hn₀, NNRat.exists]
