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.conjContinuousAlgEquiv SeminormedAddCommGroup.toAddCommGroup NontriviallyNormedField.toNormedField NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid 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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.topologicalAddGroup Algebra.to_smulCommClass Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul 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 SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup DFunLike.coe StarAlgEquiv ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.instMul ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul ContinuousLinearMap.instStarId instFunLike	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	54 math math: ContinuousAlgEquiv.map_nhds_eq, ContinuousAlgEquiv.symm_apply_eq, ContinuousAlgEquiv.symm_bijective, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, ContinuousAlgEquiv.continuousOn, ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, ContinuousAlgEquiv.continuous, ContinuousAlgEquiv.symm_trans_apply, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, ContinuousAlgEquiv.symm_map_nhds_eq, ContinuousAlgEquiv.toContinuousLinearEquiv_apply, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, ContinuousAlgEquiv.ext_iff, ContinuousAlgEquiv.continuousWithinAt, ContinuousAlgEquiv.isOpenMap, ContinuousAlgEquiv.comp_continuous_iff, ContinuousAlgEquiv.image_closure, ContinuousAlgEquiv.coe_injective, 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, 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.continuousAlgEquivClass, ContinuousAlgEquiv.image_symm_eq_preimage, ContinuousAlgEquiv.self_comp_symm, ContinuousAlgEquiv.map_eq_zero_iff, ContinuousAlgEquiv.comp_coe, ContinuousAlgEquiv.coe_coe, ContinuousAlgEquiv.preimage_symm_preimage, ContinuousAlgEquiv.cast_apply, ContinuousAlgEquiv.surjective, ContinuousAlgEquiv.comp_continuous_iff', ContinuousAlgEquiv.apply_symm_apply, ContinuousAlgEquiv.preimage_closure, ContinuousAlgEquiv.coe_apply, ContinuousAlgEquiv.image_symm_image, ContinuousAlgEquiv.continuousAt, ContinuousAlgEquiv.coe_mk, ContinuousAlgEquiv.symm_preimage_preimage, ContinuousAlgEquiv.isUniformEmbedding, ContinuousAlgEquiv.coe_refl', ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply

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