English
The principal ideals generated by non-zero-divisors form a submonoid of the non-zero-divisors ideals, closed under multiplication and containing the unit.
Русский
Главные идеалы, порожденные не нулевыми делителями, образуют подмономод внутри не нулевых делителей; замкнуты под произведением и содержат единицу.
LaTeX
$$$\\text{isPrincipalNonZeroDivisorsSubmonoid}(R) :\\; \\text{Submonoid }(\\text{Subtype }(x\\in \\text{nonZeroDivisors }(\\operatorname{Ideal}R)))$ и свойства: $((a)\\cdot(b))=(ab)$ и $ (1) $ принадлежит.$$
Lean4
/-- The non-zero-divisors principal ideals of `R` form a submonoid of `(Ideal R)⁰`. -/
def isPrincipalNonZeroDivisorsSubmonoid : Submonoid (Ideal R)⁰
where
carrier := {I | IsPrincipal I.val}
mul_mem' := by
rintro ⟨_, _⟩ ⟨_, _⟩ ⟨x, rfl⟩ ⟨y, rfl⟩
exact ⟨x * y, by simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]⟩
one_mem' := ⟨1, by simp⟩
