asIdeal — Mathlib

English

Every two-sided ideal I induces an ideal in the ambient ring, preserving the underlying set; i.e., there is a canonical left-idealization I.asIdeal of a two-sided ideal I.

Русский

Каждому двустороннему идеалу I соответствует канонический левый идеал I.asIdeal, сохраняющий множество элементов, лежащих в I.

LaTeX

$$$I:\ TwoSidedIdeal(R) \to^{\text{monotone}}\mathrm{Ideal}(R)$ is the left-ideal correspondence with carrier equal to I.$$

Lean4

/-- Every two-sided ideal is also a left ideal. -/
def asIdeal : TwoSidedIdeal R →o Ideal R
    where
  toFun
    I :=
    { carrier := I
      add_mem' := I.add_mem
      zero_mem' := I.zero_mem
      smul_mem' := fun r x hx => I.mul_mem_left r x hx }
  monotone' _ _ h _ h' := h h'

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