intCast_mem_graded — Mathlib

English

Integers embedded into the graded structure land in degree-zero as well, respecting sign.

Русский

Целые числа также лежат в нулевой компоненте, отражая знак.

LaTeX

$$$\text{intCast } z \in A_0$ for all $z \in \mathbb{Z}$$$

Lean4

theorem intCast_mem_graded [Zero ι] [AddGroupWithOne R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ)
    [SetLike.GradedOne A] (z : ℤ) : (z : R) ∈ A 0 := by
  cases z
  · rw [Int.ofNat_eq_coe, Int.cast_natCast]
    exact SetLike.natCast_mem_graded _ _
  · rw [Int.cast_negSucc]
    exact neg_mem (SetLike.natCast_mem_graded _ _)

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