homogeneous — Mathlib

English

The constructed ideal I is homogeneous with respect to the grading 𝒜; i.e., it is generated by homogeneous elements of 𝒜.

Русский

Сформированный идеал I является однородным относительно градации 𝒜; то есть он задаётся порождённым однородными элементами 𝒜.

LaTeX

$$$I = carrier(f_{deg},q) \text{ is homogeneous w.r.t. } 𝒜,$ i.e. \ IsHomogeneous(𝒜,I).$$$

Lean4

theorem homogeneous : (carrier.asIdeal f_deg hm q).IsHomogeneous 𝒜 := fun i a ha j =>
  (em (i = j)).elim (fun h => h ▸ by simpa only [proj_apply, decompose_coe, of_eq_same] using ha _) fun h => by
    simpa only [proj_apply, decompose_of_mem_ne 𝒜 (Submodule.coe_mem (decompose 𝒜 a i)) h, zero_pow hm.ne',
      map_zero] using carrier.zero_mem f_deg hm q j

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