Complex

📁 Source: Mathlib/Topology/Instances/Complex.lean

Statistics

Metric	Count
Definitions	0
Theorems subfield_eq_of_closed, uniformContinuous_ringHom_eq_id_or_conj	2
Total	2

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subfield_eq_of_closed 📖	mathematical	—	RingHom.fieldRange Real Complex Real.instDivisionRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing instNormedField ofRealHom Top.top Subfield Subfield.instTop	—	Set.range_comp subset_trans Set.instIsTransSubset DenseRange.closure_range IsDenseInducing.dense IsDenseEmbedding.toIsDenseInducing Rat.isDenseEmbedding_coe_real Set.image_univ subset_refl Set.instReflSubset image_closure_subset_closure_image continuous_ofReal IsClosed.closure_eq closure_mono Subfield.instSubfieldClass coe_algebraMap Set.range_subset_iff IsSimpleOrder.eq_bot_or_eq_top Subalgebra.isSimpleOrder_of_finrank finrank_real_complex
uniformContinuous_ringHom_eq_id_or_conj 📖	mathematical	UniformContinuous Complex Subfield NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing instNormedField SetLike.instMembership Subfield.instSetLike instUniformSpaceSubtype PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField NormedField.toField instSemiring RingHom.instFunLike	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.toOneHom RingHom.toMonoidHom DivisionRing.toDivisionSemiring Subfield.toDivisionRing Subfield.subtype CommSemiring.toSemiring instCommSemiring starRingEnd instStarRing	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalDivisionRing.toContinuousInv₀ Subfield.le_topologicalClosure uniformity_subtype Filter.comap_comap IsUniformInducing.isDenseInducing Set.image_congr Set.image_id' Subtype.prop DenseRange.comp Function.Surjective.denseRange IsDenseInducing.dense IsDenseEmbedding.toIsDenseInducing IsDenseEmbedding.subtype IsDenseEmbedding.id continuous_subtype_val IsTopologicalRing.toIsTopologicalSemiring SubfieldClass.toSubringClass Subfield.instSubfieldClass Subring.instIsTopologicalRing instT2Space instCompleteSpace subfield_eq_of_closed Subfield.isClosed_topologicalClosure Continuous.comp UniformContinuous.continuous uniformContinuous_uniformly_extend continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SetLike.coe_mem RingHom.congr_fun ringHom_eq_ofReal_of_continuous RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsDenseInducing.extend_eq RingHom.coe_rangeRestrict RingEquiv.toRingHom_eq_coe RingHom.comp_apply continuous_id ringHom_eq_id_or_conj_of_continuous

---

← Back to Index