mem_one — Mathlib

English

An element x of R lies in the submonoid generated by 1 if and only if there exists n ∈ ℕ with x = n.cast.

Русский

Элемент x ∈ R принадлежит подмоноиду, порождаемому 1, тогда и только тогда, когда существует n ∈ ℕ с x = n.cast.

LaTeX

$$$x \in (1 : AddSubmonoid R) \iff \ exists\ n: \mathbb{N}, x = (n : R)$$$

Lean4

@[simp]
theorem mem_one {x : R} : x ∈ (1 : AddSubmonoid R) ↔ ∃ n : ℕ, ↑n = x :=
  .rfl

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