multiples — Mathlib

English

Membership in the closure generated by a single element x is equivalent to the existence of an integer n such that n•x equals y.

Русский

Членство в замыкании, порождаемом элементом x, эквивалентно существованию натурального числа n, такого что n•x = y.

LaTeX

$$$ y \\in \\operatorname{closure}(\\{x\\}) \\iff \\exists n: \\mathbb{N}, n \\cdot x = y $$$

Lean4

/-- The additive submonoid generated by an element. -/
def multiples (x : A) : AddSubmonoid A :=
  AddSubmonoid.copy (AddMonoidHom.mrange (multiplesHom A x)) (Set.range (fun i => i • x : ℕ → A)) <|
    Set.ext fun n => exists_congr fun i => by simp

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