isPrincipalSubmonoid — Mathlib

English

The principal ideals of R form a submonoid of the set of ideals of R, with multiplication corresponding to product of generators and unit corresponding to span{1}.

Русский

Главные идеалы R образуют подмономод внутри множества идеалов R, умножение соответствует произведению порождающих, единица равна span{1}.

LaTeX

$$$\\text{def isPrincipalSubmonoid : Submonoid}(\\text{Ideal }R)\\; := \\{I\\mid I\\text{ is principal}\\}.$$$

Lean4

/-- The principal ideals of `R` form a submonoid of `Ideal R`. -/
def isPrincipalSubmonoid : Submonoid (Ideal R)
    where
  carrier := {I | IsPrincipal I}
  mul_mem' := by
    rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
    exact ⟨x * y, span_singleton_mul_span_singleton x y⟩
  one_mem' := ⟨1, one_eq_span⟩

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