homogeneous_zero_submodule — Mathlib

English

The zero element of the ring is homogeneous of degree zero with respect to the grading given by A.

Русский

Нулевой элемент кольца гомогенный степени ноль относительно данной градации.

LaTeX

$$SetLike.IsHomogeneousElem A 0$$

Lean4

theorem homogeneous_zero_submodule [Zero ι] [Semiring S] [AddCommMonoid R] [Module S R] (A : ι → Submodule S R) :
    SetLike.IsHomogeneousElem A (0 : R) :=
  ⟨0, Submodule.zero_mem _⟩

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