Mathlib Map

Theorems · Definition · group theory

Set.zero

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

The set 0 : Set α is defined as {0} in scope Pointwise.

Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
87 results in Mathlib
Foundations
Depth 4 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.zero_smul_set · cited by 20Set.zero_smul_setSet.singleton_zero · cited by 8Set.singleton_zeroSet.zero_subset · cited by 7Set.zero_subsetSet.addZeroClass · cited by 7Set.addZeroClassSet.mem_zero · cited by 6Set.mem_zeroFinset.coe_zero · cited by 6Finset.coe_zeroSubmodule.span_zero · cited by 6Submodule.span_zeroIdeal.span_zero · cited by 5Ideal.span_zeroSet.zero_smul_set_subset · cited by 5Set.zero_smul_set_subsetSet.image_zero · cited by 4Set.image_zeroSet.mem_sum_list_ofFn · cited by 3Set.mem_sum_list_ofFnSet.zero_nonempty · cited by 3Set.zero_nonemptySet.add_eq_zero_iff · cited by 3Set.add_eq_zero_iffSet.zero_mem_zero · cited by 2Set.zero_mem_zeroSet.smul_univ₀ · cited by 2Set.smul_univ₀Set · cited by 53352SetSet.zeroCITED BYCITES

Cites1

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

  • Setstatement · cited by 53,352

Cited by90

Results whose statement or proof uses this declaration.