Pointwise

📁 Source: Mathlib/Algebra/Order/Field/Pointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems smul_Icc, smul_Ici, smul_Ico, smul_Iic, smul_Iio, smul_Ioc, smul_Ioi, smul_Ioo	8
Total	8

LinearOrderedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Icc Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Icc PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Ici 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Ici Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Ici PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Ico Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Ico PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Iic 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Iic Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Iic PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Iio 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Iio Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Iio PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Ioc Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Ioc PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Ioi 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Ioi Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Ioi PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
smul_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero Set.Ioo Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	OrderIso.image_Ioo PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono

---

← Back to Index