Mathlib Map

Theorems · Theorem · group theory

Set.mem_zero

∀ {α : Type u_2} [inst : Zero α] {a : α}, a ∈ 0 ↔ a = 0
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
6 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.

Set.mem_finsetSum · cited by 4Set.mem_finsetSumSet.mem_sum_list_ofFn · cited by 3Set.mem_sum_list_ofFnAddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero · cited by 1AddMonoidHom.preErgodic_o…le_egauge_of_forall_ne_zero · cited by 1le_egauge_of_forall_ne_ze…Set.list_sum_mem_list_sum · cited by 1Set.list_sum_mem_list_sumSet.zero_prod_zero · cited by 0Set.zero_prod_zeroSet · cited by 53352SetSet.zero · cited by 87Set.zeroSet.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 by6

Results whose statement or proof uses this declaration.