Mathlib Map

Theorems · Inductive type

SProd

Type u → Type v → outParam (Type w) → Type (max (max u v) w)

Notation type class for the set product ×ˢ.

Defined in
Mathlib.Data.SProd
Cited by
6 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SProd.sprod · cited by 1750SProd.sprodsummable_mul_of_summable_norm' · cited by 3summable_mul_of_summable_…HasSum.sum · cited by 2HasSum.sumProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat · cited by 2ProbabilityTheory.setLInt…HasProd.sum · cited by 2HasProd.sumMeasureTheory.Measure.iInf_rat_gt_prod_Iic · cited by 2Measure.iInf_rat_gt_prod_…IsLocalHomeomorph.exists_lift_nhds · cited by 1IsLocalHomeomorph.exists_…SProd.mk.noConfusion · cited by 0mk.noConfusionSProd.casesOn · cited by 0SProd.casesOnSProd.ctorIdx · cited by 0SProd.ctorIdxSProd.noConfusion · cited by 0SProd.noConfusionSProd.noConfusionType · cited by 0SProd.noConfusionTypeSProd.recOn · cited by 0SProd.recOnSProdCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by13

Results whose statement or proof uses this declaration.