isHomogeneousElem_coe — Mathlib

English

If x is a member of the i-th graded piece A(i), then viewed as an element of the ambient ring R, x is a homogeneous element of degree i.

Русский

Если x принадлежит i-й градационной части A(i), то рассматриваемый как элемент R, x имеет однородную степень i.

LaTeX

$$$ x \in A(i) \; \implies \; \text{deg}_A(x) = i, \\ \text{equivalently } \text{IsHomogeneousElem } A (x:R) ext{ with degree } i $$$

Lean4

@[simp]
theorem isHomogeneousElem_coe {A : ι → S} {i} (x : A i) : SetLike.IsHomogeneousElem A (x : R) :=
  ⟨i, x.prop⟩

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