Mathlib Map

Theorems · Theorem · group theory

Set.zero_mem_zero

∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
2 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Zero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

balancedCore_zero_mem · cited by 2balancedCore_zero_memFilter.zero_mem_zero · cited by 2Filter.zero_mem_zeroSet · cited by 53352SetSet.zero · cited by 87Set.zeroSet.zero_mem_zeroCITED BYCITES

Cites2

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

  • Setstatement · cited by 53,352
  • Set.zerostatement · cited by 87

Cited by2

Results whose statement or proof uses this declaration.