asIdeal — Mathlib

English

The carrier gives rise to an ideal I in A, defined by I = carrier f_deg q, with the stipulations that 0 ∈ I, I is closed under addition, and I is closed under multiplication by any element of A.

Русский

Носитель carrier задаёт идеал I в A: I = carrier f_deg q; 0 ∈ I, I замкнут по сложению и по умножению на элементы A.

LaTeX

$$$I := carrier(f_{deg},q) \text{ is an ideal of } A,$ with\ 0 \in I, \ I \text{ closed under addition and } A\text{-multiplication.$$

Lean4

/-- For a prime ideal `q` in `A⁰_f`, the set `{a | aᵢᵐ/fⁱ ∈ q}` as an ideal.
-/
def asIdeal : Ideal A where
  carrier := carrier f_deg q
  zero_mem' := carrier.zero_mem f_deg hm q
  add_mem' := carrier.add_mem f_deg q
  smul_mem' := carrier.smul_mem f_deg hm q

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