Theorems · Definition · group theory

Set.addZeroClass

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

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

Defined in: Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by: 7 results in Mathlib
Foundations: Depth 11 from the axioms · uses propext, Quot.sound
Assumes: AddZeroClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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
AddZeroClassstatement and proof · cited by 1,237
Set.addproof · cited by 338
Set.zeroproof · cited by 87

Cited by13

Results whose statement or proof uses this declaration.

Set.addMonoidproof · cited by 18
Set.singletonAddMonoidHomstatement · cited by 6
convexAddSubmonoidstatement · cited by 5
convexHullAddMonoidHomstatement · cited by 4
Finset.coeAddMonoidHomstatement · cited by 4
convexHullAddMonoidHom_applystatement · cited by 0
mem_convexAddSubmonoidstatement · cited by 0
Finset.coeAddMonoidHom_applystatement · cited by 0
Set.coe_singletonAddMonoidHomstatement · cited by 0
coe_convexAddSubmonoidstatement · cited by 0
Set.singletonAddMonoidHom_applystatement · cited by 0
Set.distribSMulSetstatement · cited by 0