Documentation Verification Report

ContinuousAlgEquiv

📁 Source: Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean

Statistics

Metric	Count
Definitions `ContinuousAlgEquiv`	1
Theorems `eq_continuousLinearEquivConjContinuousAlgEquiv`, `conjContinuousAlgEquiv_surjective`, `eq_linearIsometryEquivConjStarAlgEquiv`, `instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass`	4
Total	5

ContinuousAlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_continuousLinearEquivConjContinuousAlgEquiv` 📖	mathematical	—	`ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearEquiv.conjContinuousAlgEquiv` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `continuous_of_discreteTopology` `Subsingleton.discreteTopology` `ext` `Unique.instSubsingleton` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `ContinuousAlgEquivClass.toAlgEquivClass` `continuousAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `NeZero.one` `SeparatingDual.instNontrivialContinuousLinearMapIdOfContinuousSMul` `IsBoundedSMul.continuousSMul` `RingHomCompTriple.ids` `exists_ne` `SeparatingDual.exists_ne_zero` `smul_eq_zero_iff_left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `RingHomIsometric.ids` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.topologicalAddGroup` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `ContinuousLinearMap.ext` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `SeparatingDual.exists_eq_one` `apply_symm_apply` `one_smul` `AlgEquiv.injective` `IsUnit.smul_left_cancel` `Ne.isUnit` `ContinuousLinearMap.continuous` `LinearEquiv.injective` `LinearEquiv.apply_symm_apply`

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjContinuousAlgEquiv_surjective` 📖	mathematical	—	`ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousAlgEquiv` `ContinuousLinearMap` `Semifield.toCommSemiring` `ContinuousLinearMap.semiring` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.algebra` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `conjContinuousAlgEquiv`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `IsScalarTower.left` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv`

StarAlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_linearIsometryEquivConjStarAlgEquiv` 📖	mathematical	`Continuous` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DFunLike.coe` `StarAlgEquiv` `ContinuousLinearMap.add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.instMul` `ContinuousLinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.instStarId` `instFunLike`	`LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometryEquiv.conjStarAlgEquiv`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `Subsingleton.eq_zero` `norm_zero` `ext` `Unique.instSubsingleton` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `instAlgEquivClassOfNonUnitalAlgEquivClass` `instNonUnitalAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `NeZero.one` `SeparatingDual.instNontrivialContinuousLinearMapIdOfContinuousSMul` `instSeparatingDual` `IsBoundedSMul.continuousSMul` `LinearEquiv.continuous_symm` `RingHomIsometric.ids` `ContinuousLinearMap.instCompleteSpace` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeminormedAddCommGroup.to_isUniformAddGroup` `ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv` `RingHomInvPair.instStarRingEnd` `StarHomClass.map_star` `NonUnitalStarRingHomClass.toStarHomClass` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `instStarRingEquivClass` `RingHomCompTriple.ids` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.adjoint_comp` `ContinuousAlgEquiv.ext_iff` `ContinuousLinearEquiv.coe_symm_comp_coe` `ContinuousLinearMap.comp_id` `ContinuousLinearMap.adjoint_adjoint` `Algebra.IsCentral.center_eq_bot` `Algebra.IsCentral.instContinuousLinearMap` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.IsCentral.self` `Subalgebra.mem_center_iff` `isUnit_iff_exists` `ContinuousLinearMap.comp_assoc` `ContinuousLinearEquiv.coe_comp_coe_symm` `ContinuousLinearMap.id_comp` `LinearMap.IsSymmetric.clm_adjoint_eq` `Algebra.algebraMap_eq_smul_one` `StarModule.star_smul` `ContinuousLinearMap.instStarModuleId` `IsSelfAdjoint.adjoint_conj` `IsSelfAdjoint.one` `RCLike.conj_eq_iff_re` `smul_left_injective` `IsDomain.toIsCancelMulZero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `one_ne_zero` `ContinuousLinearMap.one_def` `zero_smul` `ContinuousLinearMap.nonneg_iff_isPositive` `ContinuousLinearMap.isPositive_adjoint_comp_self` `LinearMap.IsPositive.isPositive_smul_iff` `LinearMap.isPositive_one` `one_ne_zero'` `instNontrivialLinearMapId` `RCLike.ofReal_pos` `lt_of_le_of_ne'` `ContinuousLinearMap.ext` `ContinuousLinearEquiv.apply_symm_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsRat.neg_to_eq` `Mathlib.Meta.NormNum.isRat_neg` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Real.rpow_add` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Real.rpow_neg_one` `map_inv₀` `RingHom.instRingHomClass` `one_div` `RCLike.conj_ofReal` `inv_mul_cancel₀` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Real.rpow_eq_zero` `LT.lt.le` `ne_of_gt` `ContinuousLinearMap.comp_smulₛₗ` `smul_smul` `one_smul`

(root)

Definitions

Name	Category	Theorems
`ContinuousAlgEquiv` 📖	CompData	73 math math: `ModularForm.smul_slash`, `ContinuousAlgEquiv.map_nhds_eq`, `ContinuousAlgEquiv.symm_apply_eq`, `ContinuousAlgEquiv.symm_bijective`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `UpperHalfPlane.σ_sq`, `ContinuousAlgEquiv.continuousOn`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective`, `Complex.conjCAE_apply`, `UpperHalfPlane.denom_cocycle_σ`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_apply`, `ContinuousAlgEquiv.continuous`, `ContinuousAlgEquiv.symm_trans_apply`, `UpperHalfPlane.σ_mul`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `ContinuousAlgEquiv.symm_map_nhds_eq`, `UpperHalfPlane.norm_σ`, `ContinuousAlgEquiv.toContinuousLinearEquiv_apply`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `ContinuousAlgEquiv.ext_iff`, `ContinuousAlgEquiv.continuousWithinAt`, `ContinuousAlgEquiv.isOpenMap`, `ContinuousAlgEquiv.comp_continuous_iff`, `ContinuousAlgEquiv.image_closure`, `UpperHalfPlane.σ_num`, `ContinuousAlgEquiv.coe_injective`, `UpperHalfPlane.coe_smul`, `ContinuousAlgEquiv.cast_symm_apply`, `ContinuousAlgEquiv.isClosed_image`, `ContinuousAlgEquiv.symm_comp_self`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `ContinuousAlgEquiv.image_eq_preimage_symm`, `ContinuousAlgEquiv.coe_toAlgEquiv`, `ContinuousAlgEquiv.trans_apply`, `ContinuousAlgEquiv.symm_symm_apply`, `UpperHalfPlane.σ_ofReal`, `ContinuousAlgEquiv.symm_apply_apply`, `ContinuousAlgEquiv.symm_image_image`, `ContinuousAlgEquiv.eq_symm_apply`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `ContinuousAlgEquiv.toAlgEquiv_injective`, `ContinuousAlgEquiv.refl_apply`, `ContinuousAlgEquiv.coeCLE_apply`, `ContinuousAlgEquiv.continuousAlgEquivClass`, `ContinuousAlgEquiv.image_symm_eq_preimage`, `ContinuousAlgEquiv.self_comp_symm`, `ContinuousAlgEquiv.map_eq_zero_iff`, `ContinuousAlgEquiv.comp_coe`, `ModularForm.slash_def`, `ContinuousAlgEquiv.coe_coe`, `ContinuousAlgEquiv.preimage_symm_preimage`, `ContinuousAlgEquiv.cast_apply`, `ContinuousAlgEquiv.surjective`, `ContinuousAlgEquiv.comp_continuous_iff'`, `ContinuousAlgEquiv.apply_symm_apply`, `UpperHalfPlane.σ_conj`, `ContinuousAlgEquiv.preimage_closure`, `ContinuousAlgEquiv.coe_apply`, `ContinuousAlgEquiv.image_symm_image`, `UpperHalfPlane.denom_cocycle'`, `ContinuousAlgEquiv.coe_coeCLE`, `ContinuousAlgEquiv.continuousAt`, `UpperHalfPlane.σ_eventuallyEq`, `UpperHalfPlane.σ_mul_comm`, `ContinuousAlgEquiv.coe_mk`, `ContinuousAlgEquiv.symm_preimage_preimage`, `ContinuousAlgEquiv.isUniformEmbedding`, `ContinuousAlgEquiv.coe_refl'`, `ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply`, `UpperHalfPlane.σ_denom`, `ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply`, `ModularForm.slash_apply`, `UpperHalfPlane.petersson_slash`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass` 📖	mathematical	—	`OrderIsoClass` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `ContinuousLinearMap.instLoewnerPartialOrder`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomInvPair.ids` `StarAlgEquiv.eq_linearIsometryEquivConjStarAlgEquiv` `ContinuousMapClass.map_continuous` `RingHomIsometric.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `LinearMap.isPositive_linearIsometryEquiv_conj_iff`

---

← Back to Index