Algebra

📁 Source: Mathlib/Topology/Algebra/Algebra.lean

Statistics

Metric	Count
Definitions `elemental`, `instCommSemiringSubtypeMemSubalgebraOfT2Space`, `ContinuousAlgHom`, `apply`, `codRestrict`, `comp`, `copy`, `fst`, `id`, `instFunLike`, `instMonoid`, `instMul`, `instOne`, `prod`, `prodEquiv`, `prodMap`, `rangeRestrict`, `restrictScalars`, `snd`, `toAlgHom`, `toAlgHomMonoidHom`, `toContinuousLinearMap`, `commRingTopologicalClosure`, `commSemiringTopologicalClosure`, `topologicalClosure`, `valA`, `algebraMapCLM`, `instCommRingSubtypeMemSubalgebraElementalOfT2Space`, `«term_→A[_]_»`	29
Theorems `instCompleteSpaceSubtypeMemSubalgebra`, `isClosed`, `isClosedEmbedding_coe`, `le_centralizer_centralizer`, `le_iff_mem`, `le_of_mem`, `self_mem`, `coe_codRestrict`, `coe_codRestrict_apply`, `coe_coe`, `coe_comp`, `coe_comp'`, `coe_copy`, `coe_eq_id`, `coe_fst`, `coe_fst'`, `coe_id`, `coe_id'`, `coe_inj`, `coe_mk`, `coe_mk'`, `coe_mul`, `coe_pow`, `coe_prod`, `coe_prodMap`, `coe_prodMap'`, `coe_rangeRestrict`, `coe_restrictScalars`, `coe_restrictScalars'`, `coe_snd`, `coe_snd'`, `coe_toContinuousLinearMap`, `comp_apply`, `comp_assoc`, `comp_id`, `cont`, `continuous`, `copy_eq`, `eqOn_closure_adjoin`, `ext`, `ext_iff`, `ext_on`, `ext_ring`, `ext_ring_iff`, `fst_comp_prod`, `fst_prod_snd`, `id_apply`, `id_comp`, `instAlgHomClass`, `instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass`, `instContinuousMapClass`, `map_add`, `map_neg`, `map_smul`, `map_smul_of_tower`, `map_sub`, `map_sum`, `map_zero`, `mul_apply`, `mul_def`, `one_apply`, `one_def`, `prodEquiv_apply`, `prod_apply`, `snd_comp_prod`, `toAlgHomMonoidHom_apply`, `toAlgHom_eq_coe`, `uniformContinuous`, `toSpanSingleton_one_eq_algebraMapCLM`, `topologicalClosure_map_subalgebra`, `instContinuousSMul`, `coe_valA`, `coe_valA'`, `continuousSMul`, `isClosed_topologicalClosure`, `le_topologicalClosure`, `map_topologicalClosure_le`, `topologicalClosure_adjoin_le_centralizer_centralizer`, `topologicalClosure_coe`, `topologicalClosure_comap_homeomorph`, `topologicalClosure_map`, `topologicalClosure_map_le`, `topologicalClosure_minimal`, `valA_apply`, `range_valA`, `algebraMapCLM_apply`, `algebraMapCLM_coe`, `algebraMapCLM_toLinearMap`, `coe_algebraMapCLM`, `continuousSMul_of_algebraMap`, `continuous_algebraMap`, `continuous_algebraMap_iff_smul`, `instIsTopologicalSemiringSubtypeMemSubalgebra`, `toLinearMap_algebraMapCLM`	94
Total	123

Algebra

Definitions

Name	Category	Theorems
`elemental` 📖	CompOp	7 math math: `elemental.le_iff_mem`, `elemental.isClosedEmbedding_coe`, `elemental.instCompleteSpaceSubtypeMemSubalgebra`, `elemental.le_centralizer_centralizer`, `elemental.self_mem`, `elemental.isClosed`, `elemental.le_of_mem`

Algebra.elemental

Definitions

Name	Category	Theorems
`instCommSemiringSubtypeMemSubalgebraOfT2Space` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpaceSubtypeMemSubalgebra` 📖	mathematical	—	`CompleteSpace` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.elemental` `UniformSpace.toTopologicalSpace` `instUniformSpaceSubtype`	—	`IsClosed.completeSpace_coe` `isClosed_closure`
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subalgebra` `Subalgebra.instSetLike` `Algebra.elemental`	—	`Subalgebra.isClosed_topologicalClosure`
`isClosedEmbedding_coe` 📖	mathematical	—	`Topology.IsClosedEmbedding` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.elemental` `instTopologicalSpaceSubtype`	—	`Subtype.coe_injective` `Subtype.range_coe_subtype` `isClosed`
`le_centralizer_centralizer` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Algebra.elemental` `Subalgebra.centralizer` `SetLike.coe` `Subalgebra.instSetLike` `Set` `Set.instSingletonSet`	—	`Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer`
`le_iff_mem` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Algebra.elemental` `SetLike.instMembership` `Subalgebra.instSetLike`	—	`self_mem` `le_of_mem`
`le_of_mem` 📖	mathematical	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Algebra.elemental`	—	`Subalgebra.topologicalClosure_minimal` `Algebra.adjoin_le`
`self_mem` 📖	mathematical	—	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.elemental`	—	`Subalgebra.le_topologicalClosure` `Algebra.self_mem_adjoin_singleton`

ContinuousAlgHom

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	2 math math: `coe_codRestrict`, `coe_codRestrict_apply`
`comp` 📖	CompOp	11 math math: `comp_id`, `id_comp`, `comp_apply`, `comp_assoc`, `mul_def`, `ContinuousAlgEquiv.coe_comp_coe_symm`, `coe_comp`, `fst_comp_prod`, `coe_comp'`, `snd_comp_prod`, `ContinuousAlgEquiv.coe_symm_comp_coe`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`fst` 📖	CompOp	4 math math: `coe_fst`, `coe_fst'`, `fst_comp_prod`, `fst_prod_snd`
`id` 📖	CompOp	11 math math: `comp_id`, `coe_id`, `coe_eq_id`, `id_comp`, `coe_id'`, `ContinuousAlgEquiv.coe_comp_coe_symm`, `ContinuousAlgEquiv.coe_refl`, `id_apply`, `fst_prod_snd`, `one_def`, `ContinuousAlgEquiv.coe_symm_comp_coe`
`instFunLike` 📖	CompOp	49 math math: `coe_mk'`, `coe_fst`, `toAlgHomMonoidHom_apply`, `map_smul_of_tower`, `coe_id`, `coe_eq_id`, `coe_mul`, `map_smul`, `coe_toContinuousLinearMap`, `comp_apply`, `coe_id'`, `uniformContinuous`, `map_sum`, `Subalgebra.valA_apply`, `instContinuousMapClass`, `coe_restrictScalars`, `coe_prod`, `continuous`, `mul_apply`, `ext_ring_iff`, `coe_prodMap`, `map_add`, `Subalgebra.coe_valA`, `Submodule.range_valA`, `coe_inj`, `coe_fst'`, `Subalgebra.map_topologicalClosure_le`, `coe_pow`, `id_apply`, `ext_iff`, `coe_prodMap'`, `coe_rangeRestrict`, `coe_comp`, `coe_coe`, `ContinuousAlgEquiv.coe_coe`, `coe_snd'`, `coe_restrictScalars'`, `ContinuousAlgEquiv.coe_apply`, `one_apply`, `coe_comp'`, `map_zero`, `map_sub`, `prod_apply`, `Subalgebra.coe_valA'`, `toAlgHom_eq_coe`, `coe_mk`, `coe_snd`, `instAlgHomClass`, `map_neg`
`instMonoid` 📖	CompOp	2 math math: `toAlgHomMonoidHom_apply`, `coe_pow`
`instMul` 📖	CompOp	3 math math: `coe_mul`, `mul_def`, `mul_apply`
`instOne` 📖	CompOp	2 math math: `one_apply`, `one_def`
`prod` 📖	CompOp	6 math math: `coe_prod`, `prodEquiv_apply`, `fst_comp_prod`, `fst_prod_snd`, `prod_apply`, `snd_comp_prod`
`prodEquiv` 📖	CompOp	1 math math: `prodEquiv_apply`
`prodMap` 📖	CompOp	2 math math: `coe_prodMap`, `coe_prodMap'`
`rangeRestrict` 📖	CompOp	1 math math: `coe_rangeRestrict`
`restrictScalars` 📖	CompOp	2 math math: `coe_restrictScalars`, `coe_restrictScalars'`
`snd` 📖	CompOp	4 math math: `fst_prod_snd`, `coe_snd'`, `snd_comp_prod`, `coe_snd`
`toAlgHom` 📖	CompOp	4 math math: `Subalgebra.topologicalClosure_map`, `Subalgebra.map_topologicalClosure_le`, `cont`, `toAlgHom_eq_coe`
`toAlgHomMonoidHom` 📖	CompOp	1 math math: `toAlgHomMonoidHom_apply`
`toContinuousLinearMap` 📖	CompOp	2 math math: `ContinuousAlgEquiv.toContinuousLinearMap_toContinuousLinearEquiv_eq`, `coe_toContinuousLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_codRestrict` 📖	mathematical	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `DFunLike.coe` `ContinuousAlgHom` `instFunLike`	`AlgHomClass.toAlgHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `instTopologicalSpaceSubtype` `instAlgHomClass` `codRestrict` `AlgHom.codRestrict`	—	`instAlgHomClass`
`coe_codRestrict_apply` 📖	mathematical	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `DFunLike.coe` `ContinuousAlgHom` `instFunLike`	`Subalgebra.toSemiring` `instTopologicalSpaceSubtype` `Subalgebra.algebra` `codRestrict`	—	—
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass`	—	`instAlgHomClass`
`coe_comp` 📖	mathematical	—	`AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass` `comp` `AlgHom.comp`	—	`instAlgHomClass`
`coe_comp'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `ContinuousAlgHom` `instFunLike`	`copy`	—	—
`coe_eq_id` 📖	mathematical	—	`AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass` `AlgHom.id` `id`	—	`instAlgHomClass` `coe_id`
`coe_fst` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Prod.instSemiring` `Prod.algebra` `ContinuousAlgHom` `instTopologicalSpaceProd` `instFunLike` `instAlgHomClass` `fst` `AlgHom.fst`	—	`instAlgHomClass`
`coe_fst'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `instFunLike` `fst`	—	—
`coe_id` 📖	mathematical	—	`AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass` `id` `AlgHom.id`	—	`instAlgHomClass`
`coe_id'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `id`	—	—
`coe_inj` 📖	mathematical	—	`AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass`	—	`instAlgHomClass`
`coe_mk` 📖	mathematical	`Continuous` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom`	`AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass`	—	`instAlgHomClass`
`coe_mk'` 📖	mathematical	`Continuous` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom`	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `AlgHom` `AlgHom.funLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `instMul`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `Monoid.toNatPow` `instMonoid` `Nat.iterate`	—	`hom_coe_pow`
`coe_prod` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Prod.instSemiring` `Prod.algebra` `ContinuousAlgHom` `instTopologicalSpaceProd` `instFunLike` `instAlgHomClass` `prod` `AlgHom.prod`	—	`instAlgHomClass`
`coe_prodMap` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Prod.instSemiring` `Prod.algebra` `ContinuousAlgHom` `instTopologicalSpaceProd` `instFunLike` `instAlgHomClass` `prodMap` `AlgHom.prodMap`	—	`instAlgHomClass`
`coe_prodMap'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `instFunLike` `prodMap`	—	—
`coe_rangeRestrict` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `ContinuousAlgHom` `instFunLike` `instAlgHomClass` `Subalgebra.toSemiring` `Subalgebra.algebra` `instTopologicalSpaceSubtype` `rangeRestrict` `AlgHom.rangeRestrict`	—	`instAlgHomClass`
`coe_restrictScalars` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Ring.toSemiring` `ContinuousAlgHom` `instFunLike` `instAlgHomClass` `restrictScalars` `AlgHom.restrictScalars`	—	`instAlgHomClass`
`coe_restrictScalars'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Ring.toSemiring` `instFunLike` `restrictScalars`	—	—
`coe_snd` 📖	mathematical	—	`AlgHomClass.toAlgHom` `Prod.instSemiring` `Prod.algebra` `ContinuousAlgHom` `instTopologicalSpaceProd` `instFunLike` `instAlgHomClass` `snd` `AlgHom.snd`	—	`instAlgHomClass`
`coe_snd'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `instFunLike` `snd`	—	—
`coe_toContinuousLinearMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `ContinuousLinearMap.funLike` `toContinuousLinearMap` `ContinuousAlgHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`cont` 📖	mathematical	—	`Continuous` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom` `toAlgHom`	—	—
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `ContinuousAlgHom` `instFunLike`	—	`cont`
`copy_eq` 📖	mathematical	`DFunLike.coe` `ContinuousAlgHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`eqOn_closure_adjoin` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `ContinuousAlgHom` `instFunLike`	`closure` `SetLike.coe` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin`	—	`Set.EqOn.closure` `AlgHom.eqOn_adjoin_iff` `continuous`
`ext` 📖	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike`	—	`ext`
`ext_on` 📖	—	`Dense` `SetLike.coe` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.EqOn` `DFunLike.coe` `ContinuousAlgHom` `instFunLike`	—	—	`ext` `eqOn_closure_adjoin`
`ext_ring` 📖	—	—	—	—	`instAlgHomClass` `Algebra.ext_id`
`ext_ring_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`ext_ring`
`fst_comp_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `fst` `prod`	—	`ext`
`fst_prod_snd` 📖	mathematical	—	`prod` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `fst` `snd` `id`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instAlgHomClass` 📖	mathematical	—	`AlgHomClass` `ContinuousAlgHom` `instFunLike`	—	`map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `AlgHom.commutes`
`instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass` 📖	mathematical	—	`CompleteSpace` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.equalizer` `instUniformSpaceSubtype`	—	`IsClosed.completeSpace_coe` `isClosed_eq` `ContinuousMapClass.map_continuous`
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `ContinuousAlgHom` `instFunLike`	—	`cont`
`map_add` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass`
`map_neg` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Ring.toSemiring` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass`
`map_smul` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `Algebra.toSMul`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass`
`map_smul_of_tower` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike`	—	`map_smul`
`map_sub` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Ring.toSemiring` `instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass`
`map_sum` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass`
`map_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `instAlgHomClass`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `instMul`	—	—
`mul_def` 📖	mathematical	—	`ContinuousAlgHom` `instMul` `comp`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `instFunLike` `instOne`	—	—
`one_def` 📖	mathematical	—	`ContinuousAlgHom` `instOne` `id`	—	—
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ContinuousAlgHom` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `prod`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `instFunLike` `prod`	—	—
`snd_comp_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `instTopologicalSpaceProd` `Prod.algebra` `snd` `prod`	—	`ext`
`toAlgHomMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `ContinuousAlgHom` `AlgHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid` `AlgHom.End` `MonoidHom.instFunLike` `toAlgHomMonoidHom` `AlgHomClass.toAlgHom` `instFunLike` `instAlgHomClass`	—	—
`toAlgHom_eq_coe` 📖	mathematical	—	`toAlgHom` `AlgHomClass.toAlgHom` `ContinuousAlgHom` `instFunLike` `instAlgHomClass`	—	—
`uniformContinuous` 📖	mathematical	—	`UniformContinuous` `DFunLike.coe` `ContinuousAlgHom` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `instFunLike`	—	`uniformContinuous_addMonoidHom_of_continuous` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `instAlgHomClass` `continuous`

ContinuousAlgHom.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSpanSingleton_one_eq_algebraMapCLM` 📖	mathematical	—	`toSpanSingleton` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `algebraMapCLM`	—	`ext_ring` `one_smul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`topologicalClosure_map_subalgebra` 📖	mathematical	`DenseRange` `DFunLike.coe` `ContinuousAlgHom` `ContinuousAlgHom.instFunLike` `Subalgebra.topologicalClosure` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Subalgebra.map` `AlgHomClass.toAlgHom` `ContinuousAlgHom.instAlgHomClass`	—	`ContinuousAlgHom.instAlgHomClass` `SetLike.ext'_iff` `Set.image_congr` `dense_image` `ContinuousAlgHom.continuous`

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `Algebra.toSMul`	—	`continuousSMul_of_algebraMap` `IsTopologicalSemiring.toContinuousMul` `continuous_of_discreteTopology`

Subalgebra

Definitions

Name	Category	Theorems
`commRingTopologicalClosure` 📖	CompOp	—
`commSemiringTopologicalClosure` 📖	CompOp	—
`topologicalClosure` 📖	CompOp	21 math math: `ContinuousMap.abs_mem_subalgebra_closure`, `topologicalClosure_map`, `topologicalClosure_coe`, `ContinuousMap.continuousMap_mem_subalgebra_closure_of_separatesPoints`, `topologicalClosure_minimal`, `continuousMap_mem_polynomialFunctions_closure`, `topologicalClosure_map_le`, `ContinuousMap.sup_mem_subalgebra_closure`, `ContinuousMap.inf_mem_subalgebra_closure`, `ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints`, `le_topologicalClosure`, `topologicalClosure_star_comm`, `map_topologicalClosure_le`, `ContinuousMap.comp_attachBound_mem_closure`, `polynomialFunctions.topologicalClosure`, `polynomialFunctions_closure_eq_top'`, `topologicalClosure_comap_homeomorph`, `polynomialFunctions_closure_eq_top`, `isClosed_topologicalClosure`, `StarSubalgebra.topologicalClosure_toSubalgebra_comm`, `topologicalClosure_adjoin_le_centralizer_centralizer`
`valA` 📖	CompOp	4 math math: `valA_apply`, `coe_valA`, `Submodule.range_valA`, `coe_valA'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_valA` 📖	mathematical	—	`RingHomClass.toRingHom` `ContinuousAlgHom` `Subalgebra` `SetLike.instMembership` `instSetLike` `toSemiring` `instTopologicalSpaceSubtype` `algebra` `Subsemiring` `Semiring.toNonAssocSemiring` `Subsemiring.instSetLike` `toSubsemiring` `ContinuousAlgHom.instFunLike` `Subsemiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `Subsemiring.toSemiring` `ContinuousAlgHom.instAlgHomClass` `valA` `Subsemiring.subtype`	—	`AlgHomClass.toRingHomClass` `ContinuousAlgHom.instAlgHomClass`
`coe_valA'` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Subalgebra` `SetLike.instMembership` `instSetLike` `toSemiring` `instTopologicalSpaceSubtype` `algebra` `ContinuousAlgHom.instFunLike` `valA` `RingHom` `Subsemiring` `Semiring.toNonAssocSemiring` `Subsemiring.instSetLike` `toSubsemiring` `Subsemiring.toNonAssocSemiring` `RingHom.instFunLike` `Subsemiring.subtype`	—	—
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `Subalgebra` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `instTopologicalSpaceSubtype`	—	`Subsemiring.continuousSMul`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subalgebra` `instSetLike` `topologicalClosure`	—	`isClosed_closure`
`le_topologicalClosure` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`map_topologicalClosure_le` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `AlgHomClass.toAlgHom` `ContinuousAlgHom` `ContinuousAlgHom.instFunLike` `ContinuousAlgHom.instAlgHomClass` `topologicalClosure` `ContinuousAlgHom.toAlgHom`	—	`image_closure_subset_closure_image` `ContinuousAlgHom.instAlgHomClass` `ContinuousAlgHom.continuous`
`topologicalClosure_adjoin_le_centralizer_centralizer` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `Algebra.adjoin` `centralizer` `SetLike.coe` `instSetLike`	—	`topologicalClosure_minimal` `Algebra.adjoin_le_centralizer_centralizer` `Set.isClosed_centralizer` `IsTopologicalSemiring.toContinuousMul`
`topologicalClosure_coe` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `instSetLike` `topologicalClosure` `closure`	—	—
`topologicalClosure_comap_homeomorph` 📖	mathematical	`DFunLike.coe` `AlgHom` `Ring.toSemiring` `AlgHom.funLike` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	`comap` `topologicalClosure` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`SetLike.ext'` `IsTopologicalRing.toIsTopologicalSemiring` `Homeomorph.preimage_closure`
`topologicalClosure_map` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `ContinuousAlgHom` `ContinuousAlgHom.instFunLike`	`topologicalClosure` `map` `ContinuousAlgHom.toAlgHom`	—	`SetLike.coe_injective` `IsClosedMap.closure_image_eq_of_continuous` `ContinuousAlgHom.continuous`
`topologicalClosure_map_le` 📖	mathematical	`IsClosedMap` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure` `map`	—	`IsClosedMap.closure_image_subset`
`topologicalClosure_minimal` 📖	mathematical	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`
`valA_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAlgHom` `Subalgebra` `SetLike.instMembership` `instSetLike` `toSemiring` `instTopologicalSpaceSubtype` `algebra` `ContinuousAlgHom.instFunLike` `valA`	—	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_valA` 📖	mathematical	—	`AlgHom.range` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgHomClass.toAlgHom` `ContinuousAlgHom` `instTopologicalSpaceSubtype` `ContinuousAlgHom.instFunLike` `ContinuousAlgHom.instAlgHomClass` `Subalgebra.valA`	—	`Subalgebra.range_val`

(root)

Definitions

Name	Category	Theorems
`ContinuousAlgHom` 📖	CompData	53 math math: `ContinuousAlgHom.coe_mk'`, `ContinuousAlgHom.coe_fst`, `ContinuousAlgHom.toAlgHomMonoidHom_apply`, `ContinuousAlgHom.map_smul_of_tower`, `ContinuousAlgHom.coe_id`, `ContinuousAlgHom.coe_eq_id`, `ContinuousAlgHom.coe_mul`, `ContinuousAlgHom.map_smul`, `ContinuousAlgHom.coe_toContinuousLinearMap`, `ContinuousAlgHom.comp_apply`, `ContinuousAlgHom.coe_id'`, `ContinuousAlgHom.uniformContinuous`, `ContinuousAlgHom.map_sum`, `Subalgebra.valA_apply`, `ContinuousAlgHom.mul_def`, `ContinuousAlgHom.instContinuousMapClass`, `ContinuousAlgEquiv.coe_injective`, `ContinuousAlgHom.coe_restrictScalars`, `ContinuousAlgHom.coe_prod`, `ContinuousAlgHom.continuous`, `ContinuousAlgHom.mul_apply`, `ContinuousAlgHom.ext_ring_iff`, `ContinuousAlgHom.coe_prodMap`, `ContinuousAlgHom.map_add`, `Subalgebra.coe_valA`, `Submodule.range_valA`, `ContinuousAlgHom.coe_inj`, `ContinuousAlgHom.coe_fst'`, `ContinuousAlgHom.prodEquiv_apply`, `Subalgebra.map_topologicalClosure_le`, `ContinuousAlgHom.coe_pow`, `ContinuousAlgHom.id_apply`, `ContinuousAlgHom.ext_iff`, `ContinuousAlgHom.coe_prodMap'`, `ContinuousAlgHom.coe_rangeRestrict`, `ContinuousAlgHom.coe_comp`, `ContinuousAlgHom.coe_coe`, `ContinuousAlgEquiv.coe_coe`, `ContinuousAlgHom.coe_snd'`, `ContinuousAlgHom.coe_restrictScalars'`, `ContinuousAlgEquiv.coe_apply`, `ContinuousAlgHom.one_apply`, `ContinuousAlgHom.coe_comp'`, `ContinuousAlgHom.map_zero`, `ContinuousAlgHom.map_sub`, `ContinuousAlgHom.prod_apply`, `Subalgebra.coe_valA'`, `ContinuousAlgHom.one_def`, `ContinuousAlgHom.toAlgHom_eq_coe`, `ContinuousAlgHom.coe_mk`, `ContinuousAlgHom.coe_snd`, `ContinuousAlgHom.instAlgHomClass`, `ContinuousAlgHom.map_neg`
`algebraMapCLM` 📖	CompOp	6 math math: `algebraMapCLM_coe`, `coe_algebraMapCLM`, `toLinearMap_algebraMapCLM`, `algebraMapCLM_apply`, `ContinuousLinearMap.toSpanSingleton_one_eq_algebraMapCLM`, `algebraMapCLM_toLinearMap`
`instCommRingSubtypeMemSubalgebraElementalOfT2Space` 📖	CompOp	—
`«term_→A[_]_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMapCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.toModule` `ContinuousLinearMap.funLike` `algebraMapCLM` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`algebraMapCLM_coe` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.toModule` `ContinuousLinearMap.funLike` `algebraMapCLM` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`coe_algebraMapCLM`
`algebraMapCLM_toLinearMap` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.toModule` `algebraMapCLM` `Algebra.linearMap`	—	`toLinearMap_algebraMapCLM`
`coe_algebraMapCLM` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.toModule` `ContinuousLinearMap.funLike` `algebraMapCLM` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`continuousSMul_of_algebraMap` 📖	mathematical	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`ContinuousSMul` `Algebra.toSMul`	—	`continuous_algebraMap_iff_smul`
`continuous_algebraMap` 📖	mathematical	—	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one'` `Continuous.smul` `continuous_id'` `continuous_const`
`continuous_algebraMap_iff_smul` 📖	mathematical	—	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `instTopologicalSpaceProd` `Algebra.toSMul`	—	`Algebra.smul_def` `Continuous.mul` `Continuous.comp` `continuous_fst` `continuous_snd` `continuous_algebraMap`
`instIsTopologicalSemiringSubtypeMemSubalgebra` 📖	mathematical	—	`IsTopologicalSemiring` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `instTopologicalSpaceSubtype` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Subalgebra.toSemiring`	—	`Subsemiring.topologicalSemiring`
`toLinearMap_algebraMapCLM` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.toModule` `algebraMapCLM` `Algebra.linearMap`	—	—

---

← Back to Index