natCast_mem — Mathlib

English

All natural numbers, viewed inside the ambient ring R, belong to any AddSubmonoidWithOneClass S R.

Русский

Все натуральные числа, рассматриваемые в кольце R, принадлежат любому AddSubmonoidWithOneClass S R.

LaTeX

$$$\forall n \in \mathbb{N}: (n : R) \in s$$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem natCast_mem [AddSubmonoidWithOneClass S R] (n : ℕ) : (n : R) ∈ s := by
  induction n <;> simp [zero_mem, add_mem, one_mem, *]

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