Documentation Verification Report

DualQuaternion

📁 Source: Mathlib/Algebra/DualQuaternion.lean

Statistics

Metric	Count
Definitions `dualNumberEquiv`	1
Theorems `fst_imI_dualNumberEquiv_symm`, `fst_imJ_dualNumberEquiv_symm`, `fst_imK_dualNumberEquiv_symm`, `fst_re_dualNumberEquiv_symm`, `imI_fst_dualNumberEquiv`, `imI_snd_dualNumberEquiv`, `imJ_fst_dualNumberEquiv`, `imJ_snd_dualNumberEquiv`, `imK_fst_dualNumberEquiv`, `imK_snd_dualNumberEquiv`, `re_fst_dualNumberEquiv`, `re_snd_dualNumberEquiv`, `snd_imI_dualNumberEquiv_symm`, `snd_imJ_dualNumberEquiv_symm`, `snd_imK_dualNumberEquiv_symm`, `snd_re_dualNumberEquiv_symm`	16
Total	17

Quaternion

Definitions

Name	Category	Theorems
`dualNumberEquiv` 📖	CompOp	16 math math: `snd_imJ_dualNumberEquiv_symm`, `snd_re_dualNumberEquiv_symm`, `imJ_fst_dualNumberEquiv`, `imI_fst_dualNumberEquiv`, `fst_imK_dualNumberEquiv_symm`, `imK_fst_dualNumberEquiv`, `re_fst_dualNumberEquiv`, `fst_imJ_dualNumberEquiv_symm`, `fst_imI_dualNumberEquiv_symm`, `imJ_snd_dualNumberEquiv`, `snd_imK_dualNumberEquiv_symm`, `re_snd_dualNumberEquiv`, `snd_imI_dualNumberEquiv_symm`, `fst_re_dualNumberEquiv_symm`, `imI_snd_dualNumberEquiv`, `imK_snd_dualNumberEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_imI_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.fst` `QuaternionAlgebra.imI` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`fst_imJ_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.fst` `QuaternionAlgebra.imJ` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`fst_imK_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.fst` `QuaternionAlgebra.imK` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`fst_re_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.fst` `QuaternionAlgebra.re` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imI_fst_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imI` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.fst` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imI_snd_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imI` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.snd` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imJ_fst_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imJ` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.fst` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imJ_snd_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imJ` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.snd` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imK_fst_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imK` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.fst` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`imK_snd_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.imK` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.snd` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`re_fst_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.re` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.fst` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`re_snd_dualNumberEquiv` 📖	mathematical	—	`QuaternionAlgebra.re` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.snd` `Quaternion` `DFunLike.coe` `AlgEquiv` `DualNumber` `TrivSqZeroExt.zero` `TrivSqZeroExt.one` `TrivSqZeroExt.neg` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `TrivSqZeroExt.commRing` `Semiring.toModule` `CommSemiring.toSemiring` `Semiring.toOppositeModule` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `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.left` `DistribMulAction.toMulAction` `algebra` `TrivSqZeroExt.instAlgebra` `TrivSqZeroExt.algebra'` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv`	—	`CommSemigroup.isCentralScalar` `SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`snd_imI_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.snd` `QuaternionAlgebra.imI` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`snd_imJ_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.snd` `QuaternionAlgebra.imJ` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`snd_imK_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.snd` `QuaternionAlgebra.imK` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`snd_re_dualNumberEquiv_symm` 📖	mathematical	—	`TrivSqZeroExt.snd` `QuaternionAlgebra.re` `DualNumber` `TrivSqZeroExt.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `TrivSqZeroExt.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TrivSqZeroExt.zero` `DFunLike.coe` `AlgEquiv` `Quaternion` `CommRing.toCommSemiring` `TrivSqZeroExt.semiring` `Ring.toSemiring` `instRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `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.left` `DistribMulAction.toMulAction` `TrivSqZeroExt.commRing` `CommSemiring.toSemiring` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `NonUnitalCommRing.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `algebra` `Algebra.id` `instModule` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`

---

← Back to Index