Mathlib Map

Theorems · Definition · group theory

Set.mulOneClass

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

Set α is a MulOneClass under pointwise operations if α is.

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

Around this declaration

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

Set.monoid · cited by 19Set.monoidSet.singletonMonoidHom · cited by 6Set.singletonMonoidHomFinset.coeMonoidHom · cited by 4Finset.coeMonoidHomFinset.coe_coeMonoidHom · cited by 0Finset.coe_coeMonoidHomSet.singletonMonoidHom_apply · cited by 0Set.singletonMonoidHom_ap…Set.coe_singletonMonoidHom · cited by 0Set.coe_singletonMonoidHomFinset.coeMonoidHom_apply · cited by 0Finset.coeMonoidHom_applySet · cited by 53352SetMulOneClass · cited by 1018MulOneClassSet.mul · cited by 297Set.mulSet.one · cited by 54Set.oneSet.mulOneClassCITED BYCITES

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
  • MulOneClassstatement and proof · cited by 1,018
  • Set.mulproof · cited by 297
  • Set.oneproof · cited by 54

Cited by7

Results whose statement or proof uses this declaration.