addSubmonoid_closure_range_mul_self

English

The additive submonoid generated by all square integers equals the nonnegative integers: AddSubmonoid.closure(Set.range(x ↦ x^2)) = AddSubmonoid.nonneg ℤ.

Русский

Аддитивное подмножество, порожденное всеми квадратами целых чисел, равно неотрицательным целым: AddSubmonoid.closure(Set.range(x ↦ x^2)) = AddSubmonoid.nonneg ℤ.

LaTeX

$$$\operatorname{AddSubmonoid.closure}(\operatorname{Set.range}(x \mapsto x^2)) = \operatorname{AddSubmonoid.nonneg}(\mathbb{Z})$$$

Lean4

@[simp]
theorem addSubmonoid_closure_range_mul_self : closure (range fun x : ℤ ↦ x * x) = nonneg _ := by
  simpa only [sq] using addSubmonoid_closure_range_pow even_two

Похожие утверждения