zero_mem — Mathlib

English

The zero element of A lies in the carrier for any q, i.e., 0 ∈ carrier f_deg q.

Русский

Нуль принадлежит carrier f_deg q.

LaTeX

$$$\forall R A [\text{CommRing } R] [\text{CommRing } A] [\text{Algebra } R A] \{𝒜 : \mathbb{N} \to \text{Submodule } R A\} [\text{GradedAlgebra } 𝒜] \{f : A\} {m : \mathbb{N}}(f_{deg} : f \in 𝒜(m)) \ (q : Spec.T A_f^0), 0 \in carrier(f_{deg},q).$$$

Lean4

theorem zero_mem : (0 : A) ∈ carrier f_deg q := fun i =>
  by
  convert Submodule.zero_mem q.1 using 1
  rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_zero];
  simp_rw [map_zero, zero_pow hm.ne']
  convert Localization.mk_zero (S := Submonoid.powers f) _ using 1

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