Structure hierarchy underlying NormedField

Mathlib v4.32.0-rc1-patch1 · 101 classes, 142 drawn edges (transitively reduced) · solid = extends/projection, dashed = derived instance · layout grouped by subject area
mathlib The structure hierarchy underlying NormedField in Mathlib (leanprover-community/mathlib4 v4.32.0-rc1-patch1). An edge from S to T indicates that an instance of T can be derived from an instance of S. Solid edges: `extends` parents / structure projections.  Dashed edges: derived `instance`s. Transitively derivable arrows and some arrows to the leaves (e.g. Distrib to Mul) are omitted for readability; per-class parents and fields are in tooltip_data.json. cluster_legend Legend cluster_topo cluster_topoalg cluster_normed cluster_ringth L1 normed structures L2 metric / topology L3 topological algebra L4 ring-theoretic props L5 algebraic hierarchy L6 notation / operations T2Space T2Space T1Space T1Space T2Space->T1Space CompletelyRegularSpace CompletelyRegularSpace RegularSpace RegularSpace CompletelyRegularSpace->RegularSpace PseudoEMetricSpace PseudoEMetricSpace FirstCountableTopology FirstCountableTopology PseudoEMetricSpace->FirstCountableTopology EDist EDist PseudoEMetricSpace->EDist UniformSpace UniformSpace PseudoEMetricSpace->UniformSpace Dist Dist TopologicalSpace TopologicalSpace FrechetUrysohnSpace FrechetUrysohnSpace FirstCountableTopology->FrechetUrysohnSpace SequentialSpace SequentialSpace FrechetUrysohnSpace->SequentialSpace Bornology Bornology EMetricSpace EMetricSpace EMetricSpace->PseudoEMetricSpace T0Space T0Space EMetricSpace->T0Space T1Space->T0Space MetricSpace MetricSpace MetricSpace->T2Space MetricSpace->EMetricSpace PseudoMetricSpace PseudoMetricSpace MetricSpace->PseudoMetricSpace PseudoMetricSpace->PseudoEMetricSpace PseudoMetricSpace->Dist PseudoMetricSpace->Bornology UniformSpace->CompletelyRegularSpace UniformSpace->TopologicalSpace ContinuousMul ContinuousMul IsTopologicalAddGroup IsTopologicalAddGroup ContinuousAdd ContinuousAdd IsTopologicalAddGroup->ContinuousAdd ContinuousNeg ContinuousNeg IsTopologicalAddGroup->ContinuousNeg IsTopologicalRing IsTopologicalRing IsTopologicalRing->ContinuousNeg IsTopologicalSemiring IsTopologicalSemiring IsTopologicalRing->IsTopologicalSemiring IsTopologicalSemiring->ContinuousMul IsTopologicalSemiring->ContinuousAdd IsUniformAddGroup IsUniformAddGroup IsUniformAddGroup->IsTopologicalAddGroup NormedRing NormedRing SeminormedRing SeminormedRing NormedRing->SeminormedRing NonUnitalNormedRing NonUnitalNormedRing NormedRing->NonUnitalNormedRing NonUnitalSeminormedRing NonUnitalSeminormedRing SeminormedRing->NonUnitalSeminormedRing Ring Ring SeminormedRing->Ring NormedDivisionRing NormedDivisionRing NormedDivisionRing->NormedRing NormOneClass NormOneClass NormedDivisionRing->NormOneClass NormMulClass NormMulClass NormedDivisionRing->NormMulClass DivisionRing DivisionRing NormedDivisionRing->DivisionRing NormedCommRing NormedCommRing NormedCommRing->NormedRing CommRing CommRing NormedCommRing->CommRing NormedField NormedField NormedField->NormedDivisionRing NormedField->NormedCommRing Field Field NormedField->Field NormedAddCommGroup NormedAddCommGroup NormedAddCommGroup->MetricSpace SeminormedAddCommGroup SeminormedAddCommGroup NormedAddCommGroup->SeminormedAddCommGroup NonUnitalSeminormedRing->IsTopologicalRing NonUnitalSeminormedRing->SeminormedAddCommGroup NonUnitalRing NonUnitalRing NonUnitalSeminormedRing->NonUnitalRing NonUnitalNormedRing->NormedAddCommGroup NonUnitalNormedRing->NonUnitalSeminormedRing SeminormedAddCommGroup->PseudoMetricSpace SeminormedAddCommGroup->IsUniformAddGroup Norm Norm SeminormedAddCommGroup->Norm AddCommGroup AddCommGroup SeminormedAddCommGroup->AddCommGroup EuclideanDomain EuclideanDomain IsPrincipalIdealRing IsPrincipalIdealRing EuclideanDomain->IsPrincipalIdealRing Nontrivial Nontrivial EuclideanDomain->Nontrivial EuclideanDomain->CommRing IsDomain IsDomain NoZeroDivisors NoZeroDivisors IsDomain->NoZeroDivisors IsCancelMulZero IsCancelMulZero IsDomain->IsCancelMulZero IsDomain->Nontrivial IsLocalRing IsLocalRing IsLocalRing->Nontrivial IsNoetherianRing IsNoetherianRing IsPrincipalIdealRing->IsNoetherianRing IsLeftCancelMulZero IsLeftCancelMulZero IsRightCancelMulZero IsRightCancelMulZero IsCancelMulZero->IsLeftCancelMulZero IsCancelMulZero->IsRightCancelMulZero MonoidWithZero MonoidWithZero Monoid Monoid MonoidWithZero->Monoid SemigroupWithZero SemigroupWithZero MonoidWithZero->SemigroupWithZero MulZeroOneClass MulZeroOneClass MonoidWithZero->MulZeroOneClass ZPow ZPow NonUnitalNonAssocRing NonUnitalNonAssocRing NonUnitalNonAssocSemiring NonUnitalNonAssocSemiring NonUnitalNonAssocRing->NonUnitalNonAssocSemiring NonUnitalNonAssocRing->AddCommGroup AddMonoidWithOne AddMonoidWithOne NatCast NatCast AddMonoidWithOne->NatCast One One AddMonoidWithOne->One AddMonoid AddMonoid AddMonoidWithOne->AddMonoid Distrib Distrib Sub Sub NonAssocSemiring NonAssocSemiring NonAssocSemiring->NonUnitalNonAssocSemiring AddCommMonoidWithOne AddCommMonoidWithOne NonAssocSemiring->AddCommMonoidWithOne NonAssocSemiring->MulZeroOneClass MulOneClass MulOneClass MulOne MulOne MulOneClass->MulOne AddCommSemigroup AddCommSemigroup AddCommMagma AddCommMagma AddCommSemigroup->AddCommMagma AddSemigroup AddSemigroup AddCommSemigroup->AddSemigroup AddZero AddZero Zero Zero AddZero->Zero Add Add AddZero->Add IntCast IntCast Inv Inv CommMonoid CommMonoid CommMonoid->Monoid CommSemigroup CommSemigroup CommMonoid->CommSemigroup Neg Neg Monoid->MulOneClass Semigroup Semigroup Monoid->Semigroup NPow NPow Monoid->NPow DivInvMonoid DivInvMonoid DivInvMonoid->ZPow DivInvMonoid->Inv DivInvMonoid->Monoid Div Div DivInvMonoid->Div Mul Mul Semigroup->Mul Dvd Dvd Semigroup->Dvd MulZeroClass MulZeroClass MulZeroClass->Zero NonUnitalNonAssocSemiring->Distrib NonUnitalNonAssocSemiring->MulZeroClass AddCommMonoid AddCommMonoid NonUnitalNonAssocSemiring->AddCommMonoid AddGroup AddGroup AddCommGroup->AddGroup AddCommGroup->AddCommMonoid Ring->AddCommGroup Semiring Semiring Ring->Semiring AddGroupWithOne AddGroupWithOne Ring->AddGroupWithOne NSMul NSMul AddSemigroup->Add AddZeroClass AddZeroClass AddZeroClass->AddZero NNRatCast NNRatCast SubNegMonoid SubNegMonoid AddGroup->SubNegMonoid CommSemigroup->Semigroup CommMagma CommMagma CommSemigroup->CommMagma Semiring->MonoidWithZero Semiring->NonAssocSemiring NonUnitalSemiring NonUnitalSemiring Semiring->NonUnitalSemiring MulOne->One MulOne->Mul AddCommMonoid->AddCommSemigroup AddCommMonoid->AddMonoid ZSMul ZSMul CommRing->CommMonoid CommRing->Ring RatCast RatCast SemigroupWithZero->Semigroup SemigroupWithZero->MulZeroClass Field->EuclideanDomain Field->IsLocalRing Field->DivisionRing GroupWithZero GroupWithZero GroupWithZero->MonoidWithZero GroupWithZero->Nontrivial GroupWithZero->DivInvMonoid AddGroupWithOne->AddMonoidWithOne AddGroupWithOne->IntCast AddGroupWithOne->AddGroup NonUnitalSemiring->NonUnitalNonAssocSemiring NonUnitalSemiring->SemigroupWithZero NonUnitalRing->NonUnitalNonAssocRing NonUnitalRing->NonUnitalSemiring SubNegMonoid->Sub SubNegMonoid->Neg SubNegMonoid->ZSMul SubNegMonoid->AddMonoid AddMonoid->NSMul AddMonoid->AddSemigroup AddMonoid->AddZeroClass AddCommMonoidWithOne->AddMonoidWithOne AddCommMonoidWithOne->AddCommMonoid DivisionRing->IsDomain DivisionRing->Ring DivisionRing->RatCast DivisionSemiring DivisionSemiring DivisionRing->DivisionSemiring DivisionSemiring->NNRatCast DivisionSemiring->Semiring DivisionSemiring->GroupWithZero MulZeroOneClass->MulOneClass MulZeroOneClass->MulZeroClass Ring->NonUnitalRing EMetricSpace->T2Space EuclideanDomain->IsDomain GroupWithZero->IsCancelMulZero GroupWithZero->NoZeroDivisors DivisionRing->IsPrincipalIdealRing DivisionSemiring->IsPrincipalIdealRing