DivisionRing -> GroupWithZero -> Nontrivial
BooleanAlgebra -> GeneralizedHeytingAlgebra -> HImp
CompleteLattice -> CompletePartialOrder -> OmegaCompletePartialOrder
DivisionMonoid -> DivInvOneMonoid -> DivInvMonoid
DivisionRing -> DivInvOneMonoid -> DivInvMonoid
DivisionRing -> DivisionMonoid -> DivInvMonoid
Group -> DivInvOneMonoid -> DivInvMonoid
Group -> DivisionMonoid -> DivInvMonoid
GroupWithZero -> DivInvOneMonoid -> DivInvMonoid
GroupWithZero -> DivisionMonoid -> DivInvMonoid
DivisionRing -> GroupWithZero -> DivInvMonoid
RightCancelMonoid -> MulOneClass -> FaithfulSMul
CommRing -> NonAssocRing -> AddCommGroupWithOne
GroupWithZero -> CancelMonoidWithZero -> NoZeroDivisors
EuclideanDomain -> CancelMonoidWithZero -> NoZeroDivisors
LinearOrder -> SemilatticeSup -> PartialOrder
LinearOrder -> SemilatticeInf -> PartialOrder
CompletePartialOrder -> OmegaCompletePartialOrder -> PartialOrder
NormedCommGroup -> NormedGroup -> MetricSpace
NormedAddCommGroup -> NormedAddGroup -> MetricSpace
NonUnitalNormedRing -> NormedAddGroup -> MetricSpace
NonUnitalNormedRing -> NormedAddCommGroup -> MetricSpace
NormedRing -> NonUnitalNormedRing -> MetricSpace
NormedDivisionRing -> NonUnitalNormedRing -> MetricSpace
NormedField -> NonUnitalNormedRing -> MetricSpace
NormedRing -> NormedAddGroup -> MetricSpace
NormedRing -> NormedAddCommGroup -> MetricSpace
NormedDivisionRing -> NormedRing -> MetricSpace
NormedDivisionRing -> NormedAddGroup -> MetricSpace
NormedDivisionRing -> NormedAddCommGroup -> MetricSpace
NormedField -> NormedAddGroup -> MetricSpace
NormedField -> NormedAddCommGroup -> MetricSpace
NormedField -> NormedRing -> MetricSpace
NormedField -> NormedDivisionRing -> MetricSpace
Lean.Grind.Ring -> Lean.Grind.AddCommGroup -> Neg
Denumerable -> Primcodable -> Encodable
NormedAddGroup -> SeminormedAddGroup -> Norm
NormedAddCommGroup -> SeminormedAddGroup -> Norm
SeminormedRing -> SeminormedAddGroup -> Norm
NonUnitalNormedRing -> SeminormedAddGroup -> Norm
NormedRing -> SeminormedAddGroup -> Norm
NormedDivisionRing -> SeminormedAddGroup -> Norm
NormedField -> SeminormedAddGroup -> Norm
SeminormedCommGroup -> SeminormedGroup -> Norm
NormedCommGroup -> SeminormedGroup -> Norm
NormedGroup -> SeminormedGroup -> Norm
NormedCommGroup -> NormedGroup -> Norm
SeminormedAddCommGroup -> SeminormedAddGroup -> Norm
NormedAddCommGroup -> SeminormedAddCommGroup -> Norm
SeminormedRing -> SeminormedAddCommGroup -> Norm
NonUnitalNormedRing -> SeminormedAddCommGroup -> Norm
NormedRing -> SeminormedAddCommGroup -> Norm
NormedDivisionRing -> SeminormedAddCommGroup -> Norm
NormedField -> SeminormedAddCommGroup -> Norm
NormedAddCommGroup -> NormedAddGroup -> Norm
NormedCommGroup -> SeminormedCommGroup -> Norm
NonUnitalSeminormedRing -> SeminormedAddGroup -> Norm
NonUnitalSeminormedRing -> SeminormedAddCommGroup -> Norm
SeminormedRing -> NonUnitalSeminormedRing -> Norm
NonUnitalNormedRing -> NonUnitalSeminormedRing -> Norm
NormedRing -> NonUnitalSeminormedRing -> Norm
NormedDivisionRing -> NonUnitalSeminormedRing -> Norm
NormedField -> NonUnitalSeminormedRing -> Norm
NormedDivisionRing -> SeminormedRing -> Norm
NonUnitalNormedRing -> NormedAddGroup -> Norm
NonUnitalNormedRing -> NormedAddCommGroup -> Norm
NormedRing -> NonUnitalNormedRing -> Norm
NormedDivisionRing -> NonUnitalNormedRing -> Norm
NormedField -> NonUnitalNormedRing -> Norm
NormedRing -> NormedAddGroup -> Norm
NormedRing -> NormedAddCommGroup -> Norm
NormedRing -> SeminormedRing -> Norm
NormedDivisionRing -> NormedRing -> Norm
NormedDivisionRing -> NormedAddGroup -> Norm
NormedDivisionRing -> NormedAddCommGroup -> Norm
NormedField -> NormedAddGroup -> Norm
NormedField -> NormedAddCommGroup -> Norm
NormedField -> SeminormedRing -> Norm
NormedField -> NormedRing -> Norm
NormedField -> NormedDivisionRing -> Norm
LinearOrder -> SemilatticeSup -> Max
GeneralizedHeytingAlgebra -> DistribLattice -> Lattice
LinearOrder -> DistribLattice -> Lattice
GeneralizedCoheytingAlgebra -> DistribLattice -> Lattice
CompleteLattice -> ConditionallyCompleteLattice -> Lattice
CommGroupWithZero -> CancelCommMonoidWithZero -> CommMonoidWithZero
Ring -> AddCommGroupWithOne -> AddCommGroup
Ring -> NonUnitalNonAssocRing -> AddCommGroup
Ring -> LieRing -> AddCommGroup
NormedAddCommGroup -> SeminormedAddCommGroup -> AddCommGroup
Lean.Grind.Ring -> Lean.Grind.IntModule -> Lean.Grind.AddCommGroup
PseudoMetricSpace -> PseudoEMetricSpace -> TopologicalSpace.PseudoMetrizableSpace
Ring -> AddCommGroupWithOne -> AddGroupWithOne
CStarAlgebra -> NonUnitalCStarAlgebra -> StarRing
CStarAlgebra -> NonUnitalCStarAlgebra -> CompleteSpace
NormedAddGroup -> SeminormedAddGroup -> AddGroup
CompleteLinearOrder -> CompleteDistribLattice -> BiheytingAlgebra
CompletelyDistribLattice -> CompleteDistribLattice -> BiheytingAlgebra
CompleteLinearOrder -> CompletelyDistribLattice -> BiheytingAlgebra
AddCommGroup -> AddCancelCommMonoid -> AddCommMonoid
AddCommGroup -> SubtractionCommMonoid -> AddCommMonoid
NonUnitalNormedRing -> NonUnitalSeminormedRing -> NonUnitalRing
Field -> DivisionRing -> IsDomain
Field -> Semifield -> IsDomain
Field -> EuclideanDomain -> IsDomain
CompleteLinearOrder -> LinearOrder -> Ord
ConditionallyCompleteLinearOrder -> LinearOrder -> Ord
CompleteLinearOrder -> ConditionallyCompleteLinearOrder -> Ord
CoheytingAlgebra -> GeneralizedCoheytingAlgebra -> DistribLattice
GeneralizedBooleanAlgebra -> GeneralizedCoheytingAlgebra -> DistribLattice
Order.Coframe -> GeneralizedCoheytingAlgebra -> DistribLattice
Order.Coframe -> CoheytingAlgebra -> DistribLattice
BooleanAlgebra -> GeneralizedHeytingAlgebra -> DistribLattice
BooleanAlgebra -> GeneralizedCoheytingAlgebra -> DistribLattice
BooleanAlgebra -> CoheytingAlgebra -> DistribLattice
BooleanAlgebra -> GeneralizedBooleanAlgebra -> DistribLattice
Order.Frame -> GeneralizedHeytingAlgebra -> DistribLattice
NormedGroup -> SeminormedGroup -> Group
PseudoMetricSpace -> PseudoEMetricSpace -> EDist
Lean.Grind.Ring -> Lean.Grind.AddCommGroup -> Sub
NormedCommGroup -> SeminormedCommGroup -> CommGroup
MetricSpace -> EMetricSpace -> T0Space
CommGroup -> DivisionCommMonoid -> CommMonoid
CommGroup -> CancelCommMonoid -> CommMonoid
CommSemiring -> CommMonoidWithZero -> CommMonoid
CommRing -> CommMonoidWithZero -> CommMonoid
CommRing -> CommSemiring -> CommMonoid
GroupWithZero -> CancelMonoidWithZero -> MonoidWithZero
SubtractionMonoid -> SubNegZeroMonoid -> SubNegMonoid
AddGroup -> SubNegZeroMonoid -> SubNegMonoid
AddGroup -> SubtractionMonoid -> SubNegMonoid
LinearOrderedAddCommGroupWithTop -> SubNegZeroMonoid -> SubNegMonoid
LinearOrderedAddCommGroupWithTop -> SubtractionMonoid -> SubNegMonoid
CompleteLinearOrder -> Order.Frame -> CompleteLattice
CompleteLinearOrder -> Order.Coframe -> CompleteLattice
CompleteLinearOrder -> CompletelyDistribLattice -> CompleteLattice
CompletelyDistribLattice -> Order.Frame -> CompleteLattice
CompletelyDistribLattice -> Order.Coframe -> CompleteLattice
CompleteBooleanAlgebra -> Order.Frame -> CompleteLattice
CompleteBooleanAlgebra -> Order.Coframe -> CompleteLattice
CStarAlgebra -> NonUnitalCStarAlgebra -> CStarRing
NonUnitalNormedCommRing -> NonUnitalSeminormedCommRing -> NonUnitalCommRing
GeneralizedBooleanAlgebra -> GeneralizedCoheytingAlgebra -> OrderBot
AddCancelCommMonoid -> AddCancelMonoid -> AddLeftCancelMonoid
CancelCommMonoid -> CancelMonoid -> LeftCancelMonoid
CompleteLinearOrder -> ConditionallyCompleteLinearOrder -> LinearOrder
BiheytingAlgebra -> CoheytingAlgebra -> HNot
DenselyNormedField -> NontriviallyNormedField -> NormedField
DivisionRing -> Semiring -> Module.Finite
PseudoMetricSpace -> PseudoEMetricSpace -> UniformSpace
Std.PreorderPackage -> LE -> Std.LawfulOrderLT
Preorder -> LE -> Std.LawfulOrderLT
SeminormedRing -> SeminormedAddGroup -> PseudoMetricSpace
SeminormedCommGroup -> SeminormedGroup -> PseudoMetricSpace
SeminormedAddCommGroup -> SeminormedAddGroup -> PseudoMetricSpace
SeminormedRing -> SeminormedAddCommGroup -> PseudoMetricSpace
NonUnitalSeminormedRing -> SeminormedAddGroup -> PseudoMetricSpace
NonUnitalSeminormedRing -> SeminormedAddCommGroup -> PseudoMetricSpace
SeminormedRing -> NonUnitalSeminormedRing -> PseudoMetricSpace
MetricSpace -> EMetricSpace -> TopologicalSpace.MetrizableSpace
LinearOrder -> SemilatticeInf -> Min
Field -> EuclideanDomain -> CommRing
NormedCommRing -> SeminormedCommRing -> CommRing
LeftPreLieRing -> LieAdmissibleRing -> NonUnitalNonAssocRing
RightPreLieRing -> LieAdmissibleRing -> NonUnitalNonAssocRing
BooleanAlgebra -> HeytingAlgebra -> BoundedOrder
BooleanAlgebra -> CoheytingAlgebra -> BoundedOrder
BooleanRing -> CommRing -> Ring
NormedRing -> SeminormedRing -> Ring
GeneralizedBooleanAlgebra -> GeneralizedCoheytingAlgebra -> SDiff
BiheytingAlgebra -> GeneralizedCoheytingAlgebra -> SDiff
BooleanAlgebra -> BiheytingAlgebra -> SDiff
BooleanAlgebra -> GeneralizedCoheytingAlgebra -> SDiff
BooleanAlgebra -> GeneralizedBooleanAlgebra -> SDiff
Lean.Grind.Semiring -> Lean.Grind.AddCommMonoid -> Add
Std.PreorderPackage -> LE -> Std.LawfulOrderBEq
RCLike -> MeasureTheory.MeasureSpace -> MeasurableSpace
BooleanAlgebra -> GeneralizedBooleanAlgebra -> Bot
BooleanAlgebra -> HeytingAlgebra -> HasCompl
DivisionRing -> DivisionSemiring -> NNRatCast