Documentation Verification Report

Exponential

📁 Source: Mathlib/Analysis/CStarAlgebra/Exponential.lean

Statistics

Metric	Count
Definitions `expUnitary`	1
Theorems `expUnitary`, `expUnitary_add`, `continuous_expUnitary`, `expUnitary_coe`, `expUnitary_zero`	5
Total	6

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expUnitary` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid`	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.mul` `selfAdjoint.expUnitary`	—	`expUnitary_add` `symm` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass` `add_comm`
`expUnitary_add` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid`	`selfAdjoint.expUnitary` `AddSubgroup.add` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.mul`	—	`Complex.instCharZero` `Algebra.mul_smul_comm` `Algebra.smul_mul_assoc` `eq` `NormedSpace.exp.congr_simp` `smul_add` `NormedSpace.exp_add_of_commute`

selfAdjoint

Definitions

Name	Category	Theorems
`expUnitary` 📖	CompOp	18 math math: `unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le`, `Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le`, `Unitary.mem_pathComponentOne_iff`, `expUnitaryPathToOne_apply`, `norm_sq_expUnitary_sub_one`, `Unitary.openPartialHomeomorph_symm_apply`, `Unitary.expUnitary_eq_mul_inv`, `expUnitary_zero`, `continuous_expUnitary`, `expUnitary_argSelfAdjoint`, `argSelfAdjoint_expUnitary`, `Commute.expUnitary_add`, `unitary.expUnitary_eq_mul_inv`, `unitary.mem_pathComponentOne_iff`, `Unitary.path_apply`, `Commute.expUnitary`, `expUnitary_coe`, `joined_one_expUnitary`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_expUnitary` 📖	mathematical	—	`Continuous` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `expUnitary`	—	`Complex.instCharZero` `Continuous.comp'` `NormedSpace.exp_continuous` `Continuous.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuous_subtype_val`
`expUnitary_coe` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `expUnitary` `NormedSpace.exp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `Complex` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Complex.instNormedField` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.I` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`expUnitary_zero` 📖	mathematical	—	`expUnitary` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `AddSubgroup.zero` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Submonoid.one`	—	`NormedSpace.exp.congr_simp` `smul_zero` `NormedSpace.exp_zero`

---

← Back to Index