Theorems · Definition · group theory

Set.addMonoid

{α : Type u_2} → [AddMonoid α] → AddMonoid (Set α)

Set α is an AddMonoid under pointwise operations if α is.

Defined in: Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by: 18 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
AddMonoidstatement and proof · cited by 2,864
AddZeroClassproof · cited by 1,237
AddSemigroupproof · cited by 136
Set.NSMulproof · cited by 42
Set.addZeroClassproof · cited by 7
Set.addSemigroupproof · cited by 0

Cited by22

Results whose statement or proof uses this declaration.

Set.addCommMonoidproof · cited by 25
IsAddUnit.setstatement · cited by 2
Set.nsmul_subset_nsmul_add_of_sq_subset_addstatement · cited by 2
Set.isAddUnit_iffstatement · cited by 2
Set.Nonempty.nsmulstatement · cited by 2
Set.nsmul_add_addSubgroupClosurestatement · cited by 1
Set.nsmul_right_monotonestatement · cited by 1
coe_set_nsmulstatement · cited by 1
IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sqstatement · cited by 1
Set.image_nsmulstatement · cited by 1
Set.image_nsmul_of_ne_zerostatement · cited by 1
Set.nsmul_prodstatement · cited by 0