Theorems · Definition · group theory

Submonoid.MulSaturated

{M : Type u_1} → [inst : MulOneClass M] → Submonoid M → Prop

Given a submonoid s of M, we say that s is saturated if it satisfies x * y ∈ s → x ∈ s ∧ y ∈ s. It is called MulSaturated here to be distinguished from Submonoid.PowSaturated or AddSubmonoid.NSMulSaturated, which is also called "saturated" in the literature.

Defined in

Mathlib.Algebra.Group.Submonoid.Saturation

Cited by

12 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

MulOneClass