Mathlib Map

Theorems · Definition · group theory

Set.one

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

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

Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
54 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
One
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.image_one · cited by 5Set.image_oneFinset.coe_one · cited by 4Finset.coe_oneSet.mulOneClass · cited by 4Set.mulOneClassSet.singleton_one · cited by 3Set.singleton_oneSet.mem_prod_list_ofFn · cited by 2Set.mem_prod_list_ofFnSet.mul_eq_one_iff · cited by 2Set.mul_eq_one_iffIdeal.span_one · cited by 2Ideal.span_oneSet.finite_one · cited by 1Set.finite_oneFinset.coe_list_prod · cited by 1Finset.coe_list_prodSet.singletonOneHom · cited by 1Set.singletonOneHomFilter.one_mem_one · cited by 1Filter.one_mem_oneMetric.ediam_one · cited by 1Metric.ediam_oneSet.list_prod_mem_list_prod · cited by 1Set.list_prod_mem_list_pr…MonoidHom.preErgodic_of_dense_iUnion_preimage_one · cited by 1MonoidHom.preErgodic_of_d…Set.list_prod_subset_list_prod · cited by 1Set.list_prod_subset_list…Set · cited by 53352SetSet.oneCITED 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 by56

Results whose statement or proof uses this declaration.