toTwoSided — Mathlib

English

Every two-sided ideal arises from an underlying ideal that is IsTwoSided; i.e., any two-sided ideal I can be obtained from some ideal I′ with the TwoSided property.

Русский

Любой двусторонний идеал получается как порождение некоторого идеала, обладающего свойством двусторонности.

LaTeX

$$def toTwoSided(I: Ideal R) [I.IsTwoSided] : TwoSidedIdeal R$$

Lean4

/-- Bundle an `Ideal` that is already two-sided as a `TwoSidedIdeal`. -/
def toTwoSided (I : Ideal R) [I.IsTwoSided] : TwoSidedIdeal R :=
  TwoSidedIdeal.mk' I I.zero_mem I.add_mem I.neg_mem (I.smul_mem _) (I.mul_mem_right _)

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