Theorems · Theorem · group theory

AddMemClass.add_mem

∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : Add M} {inst_1 : SetLike S M} [self : AddMemClass S M] {s : S}
  {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

A substructure satisfying AddMemClass is closed under addition.

Defined in

Mathlib.Algebra.Group.Subsemigroup.Defs

Cited by

229 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 15 definitions · uses no axioms

Assumes

AddMemClass