Theorems · Theorem · group theory

PresentedAddMonoid.closure_range_of

∀ {α : Type u_2} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop),
  AddSubmonoid.closure (Set.range (PresentedAddMonoid.of rels)) = ⊤

The generators of a presented additive monoid generate the presented additive monoid. That is, the additive submonoid closure of the set of generators equals ⊤.

Defined in

Mathlib.Algebra.PresentedMonoid.Basic

Cited by

1 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound