Documentation Verification Report

MatrixExponential

📁 Source: Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Statistics

Metric	Count
Definitions	0
Theorems `exp`, `exp`, `exp_add_of_commute`, `exp_blockDiagonal`, `exp_blockDiagonal'`, `exp_conj`, `exp_conj'`, `exp_conjTranspose`, `exp_diagonal`, `exp_neg`, `exp_nsmul`, `exp_sum_of_commute`, `exp_transpose`, `exp_units_conj`, `exp_units_conj'`, `exp_zsmul`, `isUnit_exp`	17
Total	17

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_add_of_commute` 📖	mathematical	`Commute` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing`	`NormedSpace.exp` `instRing` `instTopologicalSpaceMatrix` `topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `add` `Distrib.toAdd` `instHMulOfFintypeOfMulOfAddCommMonoid`	—	`NormedSpace.exp_add_of_commute` `instCompleteSpace`
`exp_blockDiagonal` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `instFintypeProd` `instTopologicalSpaceMatrix` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Pi.ring` `Pi.topologicalSpace` `Pi.instIsTopologicalRing` `nonUnitalNonAssocRing`	—	`topologicalRing` `Pi.instIsTopologicalRing` `NormedSpace.exp_eq_tsum_rat`
`exp_blockDiagonal'` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `Sigma.instFintype` `Sigma.instDecidableEqSigma` `instTopologicalSpaceMatrix` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `blockDiagonal'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Pi.ring` `Pi.topologicalSpace` `Pi.instIsTopologicalRing` `nonUnitalNonAssocRing`	—	`topologicalRing` `Pi.instIsTopologicalRing` `NormedSpace.exp_eq_tsum_rat`
`exp_conj` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing`	`NormedSpace.exp` `instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `inv`	—	`topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.exp.congr_simp` `coe_units_inv` `exp_units_conj`
`exp_conj'` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing`	`NormedSpace.exp` `instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `inv`	—	`topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.exp.congr_simp` `coe_units_inv` `exp_units_conj'`
`exp_conjTranspose` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `instTopologicalSpaceMatrix` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`topologicalRing` `NormedSpace.star_exp` `instT2SpaceMatrix` `instContinuousStarMatrix`
`exp_diagonal` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `instTopologicalSpaceMatrix` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Pi.ring` `Pi.topologicalSpace` `Pi.instIsTopologicalRing`	—	`topologicalRing` `Pi.instIsTopologicalRing` `NormedSpace.exp_eq_tsum_rat` `diagonal_pow`
`exp_neg` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `inv` `NormedCommRing.toCommRing`	—	`topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `nonsing_inv_eq_ringInverse` `Ring.inverse_exp` `instCompleteSpace`
`exp_nsmul` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `NormedRing.toRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `AddMonoid.toNatSMul` `addMonoid` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring`	—	`NormedSpace.exp_nsmul` `instCompleteSpace`
`exp_sum_of_commute` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Matrix` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `NormedRing.toRing`	`NormedSpace.exp` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `Finset.sum` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Finset.noncommProd` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring` `Commute.exp` `instT2SpaceMatrix` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedRing.toMetricSpace` `Set.Pairwise.of_refl` `Commute.on_refl`	—	`NormedSpace.exp_sum_of_commute` `instCompleteSpace`
`exp_transpose` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `CommRing.toRing` `instTopologicalSpaceMatrix` `topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `transpose`	—	`topologicalRing` `NormedSpace.exp_eq_tsum_rat` `transpose_tsum` `transpose_smul` `transpose_pow`
`exp_units_conj` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `NormedRing.toRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring` `Units` `Units.instInv`	—	`NormedSpace.exp_units_conj` `instCompleteSpace`
`exp_units_conj'` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `NormedRing.toRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring` `Units` `Units.instInv`	—	`exp_units_conj`
`exp_zsmul` 📖	mathematical	—	`NormedSpace.exp` `Matrix` `instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `addGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `DivInvMonoid.toZPow` `instDivInvMonoid` `NormedCommRing.toCommRing`	—	`topologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `zpow_natCast` `natCast_zsmul` `exp_nsmul` `isUnit_iff_isUnit_det` `isUnit_exp` `zpow_neg` `neg_smul` `exp_neg`
`isUnit_exp` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring` `NormedRing.toRing` `NormedSpace.exp` `instRing` `instTopologicalSpaceMatrix` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `topologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`NormedSpace.isUnit_exp` `instCompleteSpace`

Matrix.IsHermitian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	`NormedSpace.exp` `Matrix` `Matrix.instRing` `instTopologicalSpaceMatrix` `Matrix.topologicalRing`	—	`Matrix.topologicalRing` `Matrix.exp_conjTranspose`

Matrix.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp` 📖	mathematical	`Matrix.IsSymm`	`NormedSpace.exp` `Matrix` `Matrix.instRing` `CommRing.toRing` `instTopologicalSpaceMatrix` `Matrix.topologicalRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Matrix.topologicalRing` `Matrix.exp_transpose`

---

← Back to Index