Documentation Verification Report

DualNumber

📁 Source: Mathlib/Data/Matrix/DualNumber.lean

Statistics

Metric	Count
Definitions `dualNumberEquiv`	1
Theorems `dualNumberEquiv_apply`, `dualNumberEquiv_symm_apply`	2
Total	3

Matrix

Definitions

Name	Category	Theorems
`dualNumberEquiv` 📖	CompOp	2 math math: `dualNumberEquiv_symm_apply`, `dualNumberEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualNumberEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `DualNumber` `semiring` `TrivSqZeroExt.semiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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.right` `Algebra.id` `addCommMonoid` `IsScalarTower.left` `DistribMulAction.toMulAction` `instAlgebra` `TrivSqZeroExt.instAlgebra` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `CommSemiring.toNonUnitalCommSemiring` `TrivSqZeroExt.algebra'` `module` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `dualNumberEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `TrivSqZeroExt.fst` `TrivSqZeroExt.snd`	—	`SMulCommClass.opposite_mid` `IsScalarTower.right` `IsScalarTower.left` `CommSemigroup.isCentralScalar` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass`
`dualNumberEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DualNumber` `Matrix` `TrivSqZeroExt.semiring` `semiring` `CommSemiring.toSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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` `IsScalarTower.right` `Algebra.id` `TrivSqZeroExt.algebra'` `instAlgebra` `module` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `TrivSqZeroExt.instAlgebra` `CommSemigroup.isCentralScalar` `NonUnitalCommSemiring.toCommSemigroup` `CommSemiring.toNonUnitalCommSemiring` `AlgEquiv.instFunLike` `AlgEquiv.symm` `dualNumberEquiv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `TrivSqZeroExt.fst` `TrivSqZeroExt.snd`	—	`SMulCommClass.opposite_mid` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.opposite_mid` `Algebra.to_smulCommClass` `CommSemigroup.isCentralScalar`

---

← Back to Index