Documentation Verification Report

ToDirectSum

📁 Source: Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

Statistics

Metric	Count
Definitions `toDirectSum`, `toAddMonoidAlgebra`, `addMonoidAlgebraAddEquivDirectSum`, `addMonoidAlgebraAlgEquivDirectSum`, `addMonoidAlgebraEquivDirectSum`, `addMonoidAlgebraRingEquivDirectSum`	6
Theorems `toDirectSum_add`, `toDirectSum_intCast`, `toDirectSum_mul`, `toDirectSum_natCast`, `toDirectSum_neg`, `toDirectSum_ofNat`, `toDirectSum_one`, `toDirectSum_pow`, `toDirectSum_single`, `toDirectSum_sub`, `toDirectSum_toAddMonoidAlgebra`, `toDirectSum_zero`, `toAddMonoidAlgebra_add`, `toAddMonoidAlgebra_intCast`, `toAddMonoidAlgebra_mul`, `toAddMonoidAlgebra_natCast`, `toAddMonoidAlgebra_neg`, `toAddMonoidAlgebra_of`, `toAddMonoidAlgebra_ofNat`, `toAddMonoidAlgebra_one`, `toAddMonoidAlgebra_pow`, `toAddMonoidAlgebra_sub`, `toAddMonoidAlgebra_toDirectSum`, `toAddMonoidAlgebra_zero`, `addMonoidAlgebraAddEquivDirectSum_apply`, `addMonoidAlgebraAddEquivDirectSum_symm_apply`, `addMonoidAlgebraAlgEquivDirectSum_apply`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `addMonoidAlgebraEquivDirectSum_apply`, `addMonoidAlgebraEquivDirectSum_symm_apply`, `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`	32
Total	38

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`toDirectSum` 📖	CompOp	17 math math: `addMonoidAlgebraEquivDirectSum_apply`, `toDirectSum_ofNat`, `toDirectSum_single`, `toDirectSum_mul`, `toDirectSum_natCast`, `toDirectSum_zero`, `toDirectSum_add`, `toDirectSum_pow`, `toDirectSum_intCast`, `toDirectSum_sub`, `toDirectSum_neg`, `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraAddEquivDirectSum_apply`, `toDirectSum_toAddMonoidAlgebra`, `addMonoidAlgebraAlgEquivDirectSum_apply`, `toDirectSum_one`, `DirectSum.toAddMonoidAlgebra_toDirectSum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDirectSum_add` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum`	—	`Finsupp.toDFinsupp_add`
`toDirectSum_intCast` 📖	mathematical	—	`toDirectSum` `Ring.toSemiring` `AddMonoidAlgebra` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `ring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.ring` `Ring.toAddCommGroup` `Ring.directSumGRing`	—	`Finsupp.toDFinsupp_single`
`toDirectSum_mul` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.instMul` `NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring`	—	`toDirectSum_zero` `toDirectSum_add` `AddMonoidHom.map_mul_iff` `addHom_ext'` `AddMonoidHom.ext` `single_mul_single` `toDirectSum_single` `DirectSum.of_mul_of`
`toDirectSum_natCast` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.instNatCast` `Semiring.directSumGSemiring`	—	`Finsupp.toDFinsupp_single`
`toDirectSum_neg` 📖	mathematical	—	`toDirectSum` `Ring.toSemiring` `AddMonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addAddCommGroup` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.instAddCommGroup` `Ring.toAddCommGroup`	—	`Finsupp.toDFinsupp_neg`
`toDirectSum_ofNat` 📖	mathematical	—	`toDirectSum`	—	`Finsupp.toDFinsupp_single`
`toDirectSum_one` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `zero` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.instOne` `One.gOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finsupp.toDFinsupp_single`
`toDirectSum_pow` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.semiring` `Semiring.directSumGSemiring`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`toDirectSum_single` 📖	mathematical	—	`toDirectSum` `single` `DFunLike.coe` `AddMonoidHom` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of`	—	`Finsupp.toDFinsupp_single`
`toDirectSum_sub` 📖	mathematical	—	`toDirectSum` `Ring.toSemiring` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addAddCommGroup` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DirectSum.instAddCommGroup` `Ring.toAddCommGroup`	—	`Finsupp.toDFinsupp_sub`
`toDirectSum_toAddMonoidAlgebra` 📖	mathematical	—	`DirectSum.toAddMonoidAlgebra` `toDirectSum`	—	`Finsupp.toDFinsupp_toFinsupp`
`toDirectSum_zero` 📖	mathematical	—	`toDirectSum` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoidDirectSum`	—	`Finsupp.toDFinsupp_zero`

DirectSum

Definitions

Name	Category	Theorems
`toAddMonoidAlgebra` 📖	CompOp	17 math math: `toAddMonoidAlgebra_sub`, `toAddMonoidAlgebra_one`, `addMonoidAlgebraEquivDirectSum_symm_apply`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `toAddMonoidAlgebra_mul`, `toAddMonoidAlgebra_natCast`, `toAddMonoidAlgebra_zero`, `toAddMonoidAlgebra_of`, `toAddMonoidAlgebra_ofNat`, `toAddMonoidAlgebra_intCast`, `toAddMonoidAlgebra_add`, `addMonoidAlgebraAddEquivDirectSum_symm_apply`, `toAddMonoidAlgebra_pow`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`, `toAddMonoidAlgebra_neg`, `AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra`, `toAddMonoidAlgebra_toDirectSum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAddMonoidAlgebra_add` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum` `AddMonoidAlgebra` `AddMonoidAlgebra.addAddCommMonoid`	—	`DFinsupp.toFinsupp_add`
`toAddMonoidAlgebra_intCast` 📖	mathematical	—	`toAddMonoidAlgebra` `Ring.toSemiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `ring` `Ring.toAddCommGroup` `Ring.directSumGRing` `AddMonoidAlgebra` `AddMonoidAlgebra.ring`	—	`DFinsupp.toFinsupp_single`
`toAddMonoidAlgebra_mul` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra` `toAddMonoidAlgebra_toDirectSum` `AddMonoidAlgebra.toDirectSum_mul`
`toAddMonoidAlgebra_natCast` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instNatCast` `Semiring.directSumGSemiring` `AddMonoidAlgebra` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidAlgebra.nonAssocSemiring` `AddMonoid.toAddZeroClass`	—	`DFinsupp.toFinsupp_single`
`toAddMonoidAlgebra_neg` 📖	mathematical	—	`toAddMonoidAlgebra` `Ring.toSemiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `Ring.toAddCommGroup` `AddMonoidAlgebra` `AddMonoidAlgebra.addAddCommGroup`	—	`DFinsupp.toFinsupp_neg`
`toAddMonoidAlgebra_of` 📖	mathematical	—	`toAddMonoidAlgebra` `DFunLike.coe` `AddMonoidHom` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `AddMonoidAlgebra.single`	—	`DFinsupp.toFinsupp_single`
`toAddMonoidAlgebra_ofNat` 📖	mathematical	—	`toAddMonoidAlgebra`	—	`DFinsupp.toFinsupp_single`
`toAddMonoidAlgebra_one` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instOne` `One.gOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidAlgebra` `AddMonoidAlgebra.zero`	—	`DFinsupp.toFinsupp_single`
`toAddMonoidAlgebra_pow` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Semiring.directSumGSemiring` `AddMonoidAlgebra` `AddMonoidAlgebra.semiring`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`toAddMonoidAlgebra_sub` 📖	mathematical	—	`toAddMonoidAlgebra` `Ring.toSemiring` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `Ring.toAddCommGroup` `AddMonoidAlgebra` `AddMonoidAlgebra.addAddCommGroup`	—	`DFinsupp.toFinsupp_sub`
`toAddMonoidAlgebra_toDirectSum` 📖	mathematical	—	`AddMonoidAlgebra.toDirectSum` `toAddMonoidAlgebra`	—	`DFinsupp.toFinsupp_toDFinsupp`
`toAddMonoidAlgebra_zero` 📖	mathematical	—	`toAddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidAlgebra` `AddMonoidAlgebra.addAddCommMonoid`	—	`DFinsupp.toFinsupp_zero`

(root)

Definitions

Name	Category	Theorems
`addMonoidAlgebraAddEquivDirectSum` 📖	CompOp	2 math math: `addMonoidAlgebraAddEquivDirectSum_symm_apply`, `addMonoidAlgebraAddEquivDirectSum_apply`
`addMonoidAlgebraAlgEquivDirectSum` 📖	CompOp	2 math math: `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `addMonoidAlgebraAlgEquivDirectSum_apply`
`addMonoidAlgebraEquivDirectSum` 📖	CompOp	2 math math: `addMonoidAlgebraEquivDirectSum_apply`, `addMonoidAlgebraEquivDirectSum_symm_apply`
`addMonoidAlgebraRingEquivDirectSum` 📖	CompOp	2 math math: `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidAlgebraAddEquivDirectSum_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoidAlgebra.addAddCommMonoid` `instAddCommMonoidDirectSum` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addMonoidAlgebraAddEquivDirectSum` `AddMonoidAlgebra.toDirectSum`	—	—
`addMonoidAlgebraAddEquivDirectSum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDirectSum` `AddMonoidAlgebra.addAddCommMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addMonoidAlgebraAddEquivDirectSum` `DirectSum.toAddMonoidAlgebra`	—	—
`addMonoidAlgebraAlgEquivDirectSum_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `AddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.semiring` `DirectSum.semiring` `Semiring.directSumGSemiring` `AddMonoidAlgebra.algebra` `DirectSum.instAlgebra` `Algebra.toModule` `Algebra.directSumGAlgebra` `AlgEquiv.instFunLike` `addMonoidAlgebraAlgEquivDirectSum` `AddMonoidAlgebra.toDirectSum`	—	—
`addMonoidAlgebraAlgEquivDirectSum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `DirectSum.semiring` `Semiring.directSumGSemiring` `AddMonoidAlgebra.semiring` `DirectSum.instAlgebra` `Algebra.toModule` `Algebra.directSumGAlgebra` `AddMonoidAlgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `addMonoidAlgebraAlgEquivDirectSum` `DirectSum.toAddMonoidAlgebra`	—	—
`addMonoidAlgebraEquivDirectSum_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `addMonoidAlgebraEquivDirectSum` `AddMonoidAlgebra.toDirectSum`	—	—
`addMonoidAlgebraEquivDirectSum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `addMonoidAlgebraEquivDirectSum` `DirectSum.toAddMonoidAlgebra`	—	—
`addMonoidAlgebraRingEquivDirectSum_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `AddMonoidAlgebra` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum.instMul` `NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `DirectSum.instNonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `addMonoidAlgebraRingEquivDirectSum` `AddMonoidAlgebra.toDirectSum`	—	—
`addMonoidAlgebraRingEquivDirectSum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `DirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `DirectSum.instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring` `AddMonoidAlgebra.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `DirectSum.instNonUnitalNonAssocSemiring` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `addMonoidAlgebraRingEquivDirectSum` `DirectSum.toAddMonoidAlgebra`	—	—

---

← Back to Index