Documentation Verification Report

Star

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

Statistics

Metric	Count
Definitions `instStarRing`	1
Theorems `star_algebraMap`, `star_def`, `star_def'`, `star_smul`, `star_ι`	5
Total	6

CliffordAlgebra

Definitions

Name	Category	Theorems
`instStarRing` 📖	CompOp	22 math math: `spinGroup.coe_star_mul_self`, `pinGroup.coe_star_mul_self`, `CliffordAlgebraQuaternion.toQuaternion_star`, `star_def'`, `spinGroup.mul_star_self_of_mem`, `star_def`, `pinGroup.mem_unitary`, `pinGroup.star_mem`, `CliffordAlgebraQuaternion.ofQuaternion_star`, `star_smul`, `pinGroup.units_mem_iff`, `pinGroup.star_mem_iff`, `spinGroup.star_mem`, `star_ι`, `pinGroup.star_mul_self_of_mem`, `star_algebraMap`, `pinGroup.mem_iff`, `spinGroup.star_mul_self_of_mem`, `pinGroup.coe_star`, `spinGroup.coe_star`, `pinGroup.mul_star_self_of_mem`, `spinGroup.star_mem_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`star_algebraMap` 📖	mathematical	—	`Star.star` `CliffordAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `StarRing.toStarAddMonoid` `instStarRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraCliffordAlgebra`	—	`star_def` `AlgHom.commutes` `reverse.commutes`
`star_def` 📖	mathematical	—	`Star.star` `CliffordAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `StarRing.toStarAddMonoid` `instStarRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `reverse` `AlgHom` `AlgHom.funLike` `involute`	—	—
`star_def'` 📖	mathematical	—	`Star.star` `CliffordAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `StarRing.toStarAddMonoid` `instStarRing` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `involute` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `reverse`	—	`reverse_involute`
`star_smul` 📖	mathematical	—	`Star.star` `CliffordAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `StarRing.toStarAddMonoid` `instStarRing` `Algebra.toSMul` `CommRing.toCommSemiring` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `Rel` `instAlgebraCliffordAlgebra`	—	`star_def` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `LinearMap.semilinearMapClass`
`star_ι` 📖	mathematical	—	`Star.star` `CliffordAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `StarRing.toStarAddMonoid` `instStarRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `ι` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`star_def` `involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `reverse_ι`

---

← Back to Index