natCast_mem_graded — Mathlib

English

Natural numbers embedded into the graded structure sit in the degree-zero component.

Русский

Естественные числа, встроенные в структуру градации, лежат в нулевой компоненте.

LaTeX

$$$\text{natCast } n \in A_0$ for all $n \in \mathbb{N}$$$

Lean4

theorem natCast_mem_graded [Zero ι] [AddMonoidWithOne R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
    [SetLike.GradedOne A] (n : ℕ) : (n : R) ∈ A 0 := by
  induction n with
  | zero =>
    rw [Nat.cast_zero]
    exact zero_mem (A 0)
  | succ _ n_ih =>
    rw [Nat.cast_succ]
    exact add_mem n_ih (SetLike.one_mem_graded _)

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