Documentation Verification Report

Equivs

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

Statistics

Metric	Count
Definitions `Q`, `equiv`, `instCommRingCliffordAlgebraRealQ`, `ofComplex`, `toComplex`, `equiv`, `Q`, `equiv`, `ofQuaternion`, `quaternionBasis`, `toQuaternion`, `equiv`, `instCommRingCliffordAlgebraUnitOfNatQuadraticForm`	13
Theorems `Q_apply`, `equiv_apply`, `equiv_symm_apply`, `ofComplex_I`, `ofComplex_comp_toComplex`, `ofComplex_conj`, `ofComplex_toComplex`, `reverse_apply`, `reverse_eq_id`, `toComplex_comp_ofComplex`, `toComplex_involute`, `toComplex_ofComplex`, `toComplex_ι`, `equiv_symm_eps`, `equiv_ι`, `ι_mul_ι`, `Q_apply`, `equiv_apply`, `equiv_symm_apply`, `i_quaternionBasis`, `j_quaternionBasis`, `k_quaternionBasis`, `ofQuaternion_comp_toQuaternion`, `ofQuaternion_mk`, `ofQuaternion_star`, `ofQuaternion_toQuaternion`, `toQuaternion_comp_ofQuaternion`, `toQuaternion_ofQuaternion`, `toQuaternion_star`, `toQuaternion_ι`, `involute_eq_id`, `reverse_apply`, `reverse_eq_id`, `ι_eq_zero`	34
Total	47

CliffordAlgebraComplex

Definitions

Name	Category	Theorems
`Q` 📖	CompOp	13 math math: `ofComplex_conj`, `ofComplex_toComplex`, `toComplex_comp_ofComplex`, `ofComplex_I`, `equiv_symm_apply`, `toComplex_ι`, `equiv_apply`, `toComplex_involute`, `toComplex_ofComplex`, `Q_apply`, `reverse_eq_id`, `ofComplex_comp_toComplex`, `reverse_apply`
`equiv` 📖	CompOp	2 math math: `equiv_symm_apply`, `equiv_apply`
`instCommRingCliffordAlgebraRealQ` 📖	CompOp	—
`ofComplex` 📖	CompOp	7 math math: `ofComplex_conj`, `ofComplex_toComplex`, `toComplex_comp_ofComplex`, `ofComplex_I`, `equiv_symm_apply`, `toComplex_ofComplex`, `ofComplex_comp_toComplex`
`toComplex` 📖	CompOp	7 math math: `ofComplex_toComplex`, `toComplex_comp_ofComplex`, `toComplex_ι`, `equiv_apply`, `toComplex_involute`, `toComplex_ofComplex`, `ofComplex_comp_toComplex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Q_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `Real` `Real.instCommSemiring` `Real.instAddCommMonoid` `Semiring.toModule` `CommSemiring.toSemiring` `QuadraticMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Q` `Real.instNeg` `Real.instMul`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Real` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex` `Ring.toSemiring` `instRingCliffordAlgebra` `Complex.instSemiring` `instAlgebraCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `AlgEquiv.instFunLike` `equiv` `AlgHom` `AlgHom.funLike` `toComplex`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Real` `Complex` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex.instSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `instAlgebraCliffordAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `AlgHom` `AlgHom.funLike` `ofComplex`	—	—
`ofComplex_I` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `Complex` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex.instSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofComplex` `Complex.I` `LinearMap` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι` `Real.instOne`	—	`Complex.liftAux_apply_I` `CliffordAlgebra.ι_sq_scalar` `mul_one` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`ofComplex_comp_toComplex` 📖	mathematical	—	`AlgHom.comp` `Real` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex` `Ring.toSemiring` `instRingCliffordAlgebra` `Complex.instSemiring` `instAlgebraCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `ofComplex` `toComplex` `AlgHom.id`	—	`CliffordAlgebra.hom_ext` `LinearMap.ext_ring` `RingHomCompTriple.ids` `toComplex_ι` `one_smul` `ofComplex_I`
`ofComplex_conj` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `Complex` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex.instSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofComplex` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing` `CommRing.toCommSemiring` `CliffordAlgebra.involute`	—	`AlgEquiv.injective` `equiv_apply` `toComplex_involute` `toComplex_ofComplex`
`ofComplex_toComplex` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `Complex` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex.instSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofComplex` `toComplex`	—	`AlgHom.congr_fun` `ofComplex_comp_toComplex`
`reverse_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Real` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `Real.instAddCommGroup` `Semiring.toModule` `Real.instCommSemiring` `Q` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.reverse`	—	`CliffordAlgebra.induction` `CliffordAlgebra.reverse.commutes` `CliffordAlgebra.reverse_ι` `CliffordAlgebra.reverse.map_mul` `mul_comm` `LinearMap.map_add`
`reverse_eq_id` 📖	mathematical	—	`CliffordAlgebra.reverse` `Real` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `LinearMap.id` `CliffordAlgebra` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra`	—	`LinearMap.ext` `reverse_apply`
`toComplex_comp_ofComplex` 📖	mathematical	—	`AlgHom.comp` `Real` `Complex` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex.instSemiring` `Ring.toSemiring` `instRingCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `instAlgebraCliffordAlgebra` `toComplex` `ofComplex` `AlgHom.id`	—	`Complex.algHom_ext` `ofComplex_I` `toComplex_ι` `one_smul`
`toComplex_involute` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex` `Ring.toSemiring` `instRingCliffordAlgebra` `Complex.instSemiring` `instAlgebraCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `AlgHom.funLike` `toComplex` `CommRing.toCommSemiring` `CliffordAlgebra.involute` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	`CliffordAlgebra.involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `toComplex_ι` `one_smul` `Complex.conj_I` `CliffordAlgebra.hom_ext` `LinearMap.ext_ring` `RingHomCompTriple.ids` `AlgHom.congr_fun`
`toComplex_ofComplex` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex` `Ring.toSemiring` `instRingCliffordAlgebra` `Complex.instSemiring` `instAlgebraCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `AlgHom.funLike` `toComplex` `ofComplex`	—	`AlgHom.congr_fun` `toComplex_comp_ofComplex`
`toComplex_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `CliffordAlgebra` `Real.commRing` `Real.instAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `Real.instCommSemiring` `Q` `Complex` `Ring.toSemiring` `instRingCliffordAlgebra` `Complex.instSemiring` `instAlgebraCliffordAlgebra` `Algebra.complexToReal` `Algebra.id` `Complex.instCommSemiring` `AlgHom.funLike` `toComplex` `LinearMap` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι` `Algebra.toSMul` `Complex.I`	—	`CliffordAlgebra.lift_ι_apply`

CliffordAlgebraDualNumber

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	2 math math: `equiv_symm_eps`, `equiv_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_symm_eps` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DualNumber` `CliffordAlgebra` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TrivSqZeroExt.semiring` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `Algebra.id` `Ring.toSemiring` `instRingCliffordAlgebra` `TrivSqZeroExt.instAlgebra` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `instAlgebraCliffordAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `DualNumber.eps` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `LinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι`	—	`DualNumber.lift_apply_eps`
`equiv_ι` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DualNumber` `Ring.toSemiring` `instRingCliffordAlgebra` `TrivSqZeroExt.semiring` `Semiring.toOppositeModule` `SMulCommClass.opposite_mid` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `Algebra.id` `instAlgebraCliffordAlgebra` `TrivSqZeroExt.instAlgebra` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `AlgEquiv.instFunLike` `equiv` `LinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι` `TrivSqZeroExt.smul` `Algebra.toSMul` `DualNumber.eps` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`CliffordAlgebra.lift_ι_apply` `DualNumber.inr_eq_smul_eps`
`ι_mul_ι` 📖	mathematical	—	`CliffordAlgebra` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `DFunLike.coe` `LinearMap` `RingHom.id` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.ι` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_one` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `smul_mul_smul_comm` `IsScalarTower.right` `CliffordAlgebra.instIsScalarTower` `IsScalarTower.left` `Algebra.to_smulCommClass` `CliffordAlgebra.ι_sq_scalar` `QuadraticMap.zero_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `smul_zero`

CliffordAlgebraQuaternion

Definitions

Name	Category	Theorems
`Q` 📖	CompOp	14 math math: `j_quaternionBasis`, `toQuaternion_star`, `toQuaternion_ofQuaternion`, `k_quaternionBasis`, `i_quaternionBasis`, `equiv_apply`, `equiv_symm_apply`, `ofQuaternion_star`, `toQuaternion_comp_ofQuaternion`, `ofQuaternion_mk`, `ofQuaternion_comp_toQuaternion`, `toQuaternion_ι`, `Q_apply`, `ofQuaternion_toQuaternion`
`equiv` 📖	CompOp	2 math math: `equiv_apply`, `equiv_symm_apply`
`ofQuaternion` 📖	CompOp	7 math math: `toQuaternion_ofQuaternion`, `equiv_symm_apply`, `ofQuaternion_star`, `toQuaternion_comp_ofQuaternion`, `ofQuaternion_mk`, `ofQuaternion_comp_toQuaternion`, `ofQuaternion_toQuaternion`
`quaternionBasis` 📖	CompOp	3 math math: `j_quaternionBasis`, `k_quaternionBasis`, `i_quaternionBasis`
`toQuaternion` 📖	CompOp	7 math math: `toQuaternion_star`, `toQuaternion_ofQuaternion`, `equiv_apply`, `toQuaternion_comp_ofQuaternion`, `ofQuaternion_comp_toQuaternion`, `toQuaternion_ι`, `ofQuaternion_toQuaternion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Q_apply` 📖	mathematical	—	`DFunLike.coe` `QuadraticForm` `CommRing.toCommSemiring` `Prod.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Prod.instModule` `CommSemiring.toSemiring` `Semiring.toModule` `QuadraticMap.instFunLike` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Q` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Ring.toSemiring` `instRingCliffordAlgebra` `QuaternionAlgebra.instRing` `instAlgebraCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `equiv` `AlgHom` `AlgHom.funLike` `toQuaternion`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Q` `Ring.toSemiring` `QuaternionAlgebra.instRing` `instRingCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `instAlgebraCliffordAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `AlgHom` `AlgHom.funLike` `ofQuaternion`	—	—
`i_quaternionBasis` 📖	mathematical	—	`QuaternionAlgebra.Basis.i` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `quaternionBasis` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `LinearMap.instFunLike` `CliffordAlgebra.ι` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`j_quaternionBasis` 📖	mathematical	—	`QuaternionAlgebra.Basis.j` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `quaternionBasis` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `LinearMap.instFunLike` `CliffordAlgebra.ι` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`k_quaternionBasis` 📖	mathematical	—	`QuaternionAlgebra.Basis.k` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `quaternionBasis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `LinearMap.instFunLike` `CliffordAlgebra.ι` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`ofQuaternion_comp_toQuaternion` 📖	mathematical	—	`AlgHom.comp` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Ring.toSemiring` `instRingCliffordAlgebra` `QuaternionAlgebra.instRing` `instAlgebraCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `ofQuaternion` `toQuaternion` `AlgHom.id`	—	`CliffordAlgebra.hom_ext` `LinearMap.prod_ext` `RingHomCompTriple.ids` `LinearMap.ext_ring` `toQuaternion_ι` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_smul` `zero_add` `zero_smul` `add_zero`
`ofQuaternion_mk` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Q` `Ring.toSemiring` `QuaternionAlgebra.instRing` `instRingCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofQuaternion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Algebra.toSMul` `RingQuot.instSemiring` `TensorAlgebra` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra` `CliffordAlgebra.Rel` `LinearMap` `RingHom.id` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toMul`	—	—
`ofQuaternion_star` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Q` `Ring.toSemiring` `QuaternionAlgebra.instRing` `instRingCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofQuaternion` `Star.star` `QuaternionAlgebra.instStarQuaternionAlgebra` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `CliffordAlgebra.instStarRing`	—	`AlgEquiv.injective` `equiv_apply` `toQuaternion_star` `toQuaternion_ofQuaternion`
`ofQuaternion_toQuaternion` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Q` `Ring.toSemiring` `QuaternionAlgebra.instRing` `instRingCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `instAlgebraCliffordAlgebra` `AlgHom.funLike` `ofQuaternion` `toQuaternion`	—	`AlgHom.congr_fun` `ofQuaternion_comp_toQuaternion`
`toQuaternion_comp_ofQuaternion` 📖	mathematical	—	`AlgHom.comp` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `Q` `Ring.toSemiring` `QuaternionAlgebra.instRing` `instRingCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `instAlgebraCliffordAlgebra` `toQuaternion` `ofQuaternion` `AlgHom.id`	—	`QuaternionAlgebra.hom_ext` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_smul` `zero_add` `zero_smul` `add_zero` `toQuaternion_ι`
`toQuaternion_ofQuaternion` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Ring.toSemiring` `instRingCliffordAlgebra` `QuaternionAlgebra.instRing` `instAlgebraCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike` `toQuaternion` `ofQuaternion`	—	`AlgHom.congr_fun` `toQuaternion_comp_ofQuaternion`
`toQuaternion_star` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Ring.toSemiring` `instRingCliffordAlgebra` `QuaternionAlgebra.instRing` `instAlgebraCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike` `toQuaternion` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `CliffordAlgebra.instStarRing` `QuaternionAlgebra.instStarQuaternionAlgebra`	—	`CliffordAlgebra.star_def'` `CliffordAlgebra.induction` `CliffordAlgebra.reverse.commutes` `AlgHom.commutes` `QuaternionAlgebra.star_coe` `CliffordAlgebra.reverse_ι` `CliffordAlgebra.involute_ι` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `toQuaternion_ι` `neg_zero` `MulZeroClass.zero_mul` `add_zero` `CliffordAlgebra.reverse.map_mul` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `StarMul.star_mul` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `NonUnitalAlgHomClass.instLinearMapClass` `StarAddMonoid.star_add`
`toQuaternion_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CliffordAlgebra` `Prod.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Prod.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Q` `QuaternionAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Ring.toSemiring` `instRingCliffordAlgebra` `QuaternionAlgebra.instRing` `instAlgebraCliffordAlgebra` `QuaternionAlgebra.instAlgebra` `Algebra.id` `AlgHom.funLike` `toQuaternion` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `LinearMap.instFunLike` `CliffordAlgebra.ι`	—	`CliffordAlgebra.lift_ι_apply`

CliffordAlgebraRing

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`instCommRingCliffordAlgebraUnitOfNatQuadraticForm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`involute_eq_id` 📖	mathematical	—	`CliffordAlgebra.involute` `PUnit.addCommGroup` `PUnit.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AlgHom.id` `CliffordAlgebra` `Ring.toSemiring` `instRingCliffordAlgebra` `instAlgebraCliffordAlgebra`	—	`CliffordAlgebra.hom_ext` `LinearMap.ext` `RingHomCompTriple.ids` `LinearMap.comp.congr_simp` `ι_eq_zero` `LinearMap.comp_zero`
`reverse_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CliffordAlgebra` `PUnit.addCommGroup` `PUnit.module` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instFunLike` `CliffordAlgebra.reverse`	—	`CliffordAlgebra.induction` `CliffordAlgebra.reverse.commutes` `ι_eq_zero` `LinearMap.zero_apply` `LinearMap.map_zero` `CliffordAlgebra.reverse.map_mul` `mul_comm` `LinearMap.map_add`
`reverse_eq_id` 📖	mathematical	—	`CliffordAlgebra.reverse` `PUnit.addCommGroup` `PUnit.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearMap.id` `CliffordAlgebra` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra`	—	`LinearMap.ext` `reverse_apply`
`ι_eq_zero` 📖	mathematical	—	`CliffordAlgebra.ι` `PUnit.addCommGroup` `PUnit.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `QuadraticForm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearMap` `RingHom.id` `CliffordAlgebra` `AddCommGroup.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `Algebra.toModule` `Ring.toSemiring` `instAlgebraCliffordAlgebra` `LinearMap.instZero`	—	`Unique.instSubsingleton`

---

← Back to Index