Documentation

LeanPool.ConwayRefinement.Imports

return to top

source

Imports

Init
LeanPool.ConwayRefinement
LeanPool.ConwayRefinement.CombinatorialGames
LeanPool.ConwayRefinement.ConwayRefinement
LeanPool.ConwayRefinement.Solution
LeanPool.ConwayRefinement.CombinatorialGames.Game
LeanPool.ConwayRefinement.CombinatorialGames.Mathlib
LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal
LeanPool.ConwayRefinement.CombinatorialGames.Surreal
LeanPool.ConwayRefinement.CombinatorialGames.Tactic
LeanPool.ConwayRefinement.ConwayRefinement.Algebra
LeanPool.ConwayRefinement.ConwayRefinement.Blueprint
LeanPool.ConwayRefinement.ConwayRefinement.Data
LeanPool.ConwayRefinement.ConwayRefinement.Examples
LeanPool.ConwayRefinement.ConwayRefinement.FieldTheory
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.Order
LeanPool.ConwayRefinement.ConwayRefinement.RingTheory
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory
LeanPool.ConwayRefinement.ConwayRefinement.Standalone
LeanPool.ConwayRefinement.ConwayRefinement.Surreal
LeanPool.ConwayRefinement.ConwayRefinement.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Topology
LeanPool.ConwayRefinement.CombinatorialGames.Game.Basic
LeanPool.ConwayRefinement.CombinatorialGames.Game.Birthday
LeanPool.ConwayRefinement.CombinatorialGames.Game.Classes
LeanPool.ConwayRefinement.CombinatorialGames.Game.Functor
LeanPool.ConwayRefinement.CombinatorialGames.Game.IGame
LeanPool.ConwayRefinement.CombinatorialGames.Game.Ordinal
LeanPool.ConwayRefinement.CombinatorialGames.Game.Player
LeanPool.ConwayRefinement.CombinatorialGames.Game.Special
LeanPool.ConwayRefinement.CombinatorialGames.Mathlib.Dyadic
LeanPool.ConwayRefinement.CombinatorialGames.Mathlib.Small
LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Basic
LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Basic
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Birthday
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Division
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Dyadic
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.HahnSeries
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Leading
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Multiplication
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Ordinal
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Pow
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Real
LeanPool.ConwayRefinement.CombinatorialGames.Tactic.AddInstances
LeanPool.ConwayRefinement.CombinatorialGames.Tactic.GameCmp
LeanPool.ConwayRefinement.CombinatorialGames.Tactic.OrdinalAlias
LeanPool.ConwayRefinement.CombinatorialGames.Tactic.Register
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GeometricIntegrality
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MonoidAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Ring
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation
LeanPool.ConwayRefinement.ConwayRefinement.Data.Multiset
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger
LeanPool.ConwayRefinement.ConwayRefinement.FieldTheory.LatticeFactorCoefficients
LeanPool.ConwayRefinement.ConwayRefinement.FieldTheory.LaurentFactorCoefficients
LeanPool.ConwayRefinement.ConwayRefinement.FieldTheory.MonicFactorCoefficients
LeanPool.ConwayRefinement.ConwayRefinement.FieldTheory.RelativeAlgebraicClosure
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.ArchimedeanSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationDomainEmbedding
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationDomainEquiv
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationResidue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CharZero
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CoefficientMap
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.ConvexFactorSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.ConvexQuotientSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DegreeTermCount
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DegreeValuation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Domain
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DomainEmbedding
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DomainEquiv
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DomainOrderType
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.EPrimitive
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FactorCoefficients
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportConstantTermOne
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportMonoidAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportNormalization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportNormalizedGCD
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportResidue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportScalarExtension
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportScalarTensor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Iterate
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IterateOrderType
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.LimitTailQuotient
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Monomial
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Multiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Negative
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NegativeMonomialIdeal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Nonpositive
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NonpositiveCoefficientMap
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NonpositiveDomainEquiv
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderedIntervalSum
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.RealSupportSupremum
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SeparatedPieceSum
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SeparatedSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SourceStatements
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SubgroupAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SubgroupGCD
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SubgroupSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SupportArchimedeanClasses
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SupportSupremum
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Translation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Truncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.TruncationIntegerPartPrimal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.WeakNormalForm
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.AlgebraicIndependentDet
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.FiniteSpanRelation
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.IndicatorFinsupp
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.TensorProduct
LeanPool.ConwayRefinement.ConwayRefinement.Order.Archimedean
LeanPool.ConwayRefinement.ConwayRefinement.Order.DifferenceAvoidance
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter
LeanPool.ConwayRefinement.ConwayRefinement.RingTheory.LaurentTower
LeanPool.ConwayRefinement.ConwayRefinement.RingTheory.LocalizationUFM
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.FinitePWOUnion
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ArchimedeanAssumptions
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Cardinal
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.CutFilling
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.RationalTailQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.RealArchimedeanStratum
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.RealModule
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Round
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.SmallDiscrete
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC
LeanPool.ConwayRefinement.ConwayRefinement.Tests.SourceIndex
LeanPool.ConwayRefinement.ConwayRefinement.Tests.UpstreamReuse
LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixson
LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonProduct
LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonRank
LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonReconstruction
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Tests
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Birthday.Basic
LeanPool.ConwayRefinement.CombinatorialGames.Surreal.HahnSeries.Basic
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermChainRule
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermFinitePartIdeal
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermPolynomial
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermSuccessorStep
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermSyzygy
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.HomogeneousDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.HomogeneousPrime
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.InternalGrading
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.LeadingGrade
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.TrailingGrade
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.DenominatorIdeal
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.MaximalDivisor
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalPreimage
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalProduct
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Refinement
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Finset.FilterCard
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.Extension
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.FinitePartSubstitution
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.HomogeneousSpan
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.HomogeneousZeroDivisors
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.OrdinalGenerators
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.BaseChange
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Correction
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.FilteredModule
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Grading
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.IdealGEGraded
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Mu
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Polynomial
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MonoidAlgebra.LatticeFunctional
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MonoidAlgebra.SingleZeroFactors
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.BaseChange
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Components
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.ComponentsSpan
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Expansion
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.FinitePartDecomposition
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.FinitePartErasure
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.FinitePartVars
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.GCDMonoid
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.LimitOrdinalContradiction
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.MapWeight
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.OrdinalDerivation
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.OrdinalExpansion
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.RemainderBound
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Syzygy
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.TermDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.WeightedTotalDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.ArchimedeanBall
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.ArchimedeanQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.ConvexQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Ring.Hom
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Tests.GeometricIntegrality
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedValuation
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.BasisOver
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGraded
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedMap
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeInitialForm
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeOver
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreePrincipalInitialIdeal
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeRepresentatives
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeScalar
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeSum
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeWeightedPolynomial
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.FiltrationDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.MaxAddDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.OfValuation
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.QuotientDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.RV
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Residue
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.ResidueMathlib
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Data.Multiset.SelectionComplexity
LeanPool.ConwayRefinement.ConwayRefinement.Data.Multiset.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.DegreeTwoNormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.DegreeTwoPrime
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.OneRowNormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.OneRowPrime
LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.ZFCDegreeTwoPrime
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.PrincipalMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.SupportSupremumMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.AlmostIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.AlmostIrreducibleFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.FiniteSupportFactorUniqueness
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.GermLike
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.GradedDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.InfiniteSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.MaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.MaximalFiniteMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedHPart
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedHPartMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedHPartSeries
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedSeriesMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PreSchreier
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalSubringLocalization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalSubringPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVGradedMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesMaximalFinite
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesMaximalMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Assumptions
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.CardinalFiniteClassReduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.CardinalIntegerPartSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.CardinalPrimalityTransfer
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.CardinalProposition922
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.CardinalSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ClassTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.FiniteClassPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.FiniteClassReduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.IntegerPartSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.IrreducibilityTransfer
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.LimitTailPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.PrimalityTransfer
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Reduced
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ReducedCharacterization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ReducedDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ReducedPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Reduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.SplitTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.TruncationDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.TruncationPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CoefficientMap
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ComplexityDecrease
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ConvolutionList
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ConvolutionRemainder
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPoint
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPointExistence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.FormalExpression
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermValueCut
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Irreducibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.LeibnizRemainder
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OneRow
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrderTypeMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueValuation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PowerRemainder
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponent
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentTensor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubring
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringFiniteSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringFraction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringFractionAlgebraic
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringLocalization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringMonoidAlgebra
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringScalarRedistributionProof
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringTensor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PurePowerRemainder
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPoint
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointCofinality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointOrderType
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointTail
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointWellOrdered
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Truncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.TruncationDrop
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.CompleteGerm
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.CompleteGermOfCauchyComplete
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.InitialForms
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.PolynomialPresentation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.PolynomialRing
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.Tests
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.Consequences
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.DegreeOne
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.GCDMonoid
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.OrdinalValueQuotient
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.Primality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.Random
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.SupportOrderTypeFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.ArchimedeanSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.CardinalTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.FiniteSupportGCD
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.FiniteSupportResidue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.FiniteSupportScalarExtension
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Iterate
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Multiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.NegativePresentation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.NonpositiveDomainEquiv
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.OrderTypeDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.PrincipalAddition
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Truncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.TruncationIntegerPartPrimal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.WeakNormalForm
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.TensorProduct.Content
LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.TensorProduct.SubalgebraBasis
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.Germ
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.Tests
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AlgebraicOrder
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.CantorBendixson
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.CantorTermCount
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.FinitePart
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.GeneralFactorization
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.IncreasingSequenceUnion
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.LeastTerm
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.LeastTermSup
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.MultiplicativelyPrincipal
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalOrder
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPowerFactorization
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPrincipal
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.OrderedUnion
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.PairBounds
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Separation
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Split
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SuccessorFactorization
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Sumset
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.Game
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.GameOperations
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.ConwayRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.ConwayRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.PrincipalRVAlgebraicIndependence
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.PrincipalRVAlgebraicIndependenceProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.CompleteHahnGerm
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.CompleteHahnGermProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.GermPolynomialRing
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.GermPolynomialRingProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnIntegerPartRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnIntegerPartRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnSeriesGCD
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnSeriesGCDProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnSeriesPolynomialRing
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnSeriesPolynomialRingProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.InlineConwayRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.InlineConwayRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.CardinalIntegerPart
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Degree
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.DegreeTransfer
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Full
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.IntegerPart
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Multiplication
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormAdd
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormBasic
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormMul
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormRecursion
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormSupport
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.RealLeadingSplit
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.SignedFull
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Transfer
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Basic
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Ordinal
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Refinement
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.RefinementConjecture
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Tests.ArchimedeanAssumptions
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Tests.RealModule
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Basic
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Cuts
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Identification
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.OmnificCodes
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.OmnificInteger
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Properness
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Reduced
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Refinement
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.ArchimedeanBallBase
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CantorBendixsonAddition
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CantorBendixsonConvexCover
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.ClosedPWO
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CoinitialComplete
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.OrderedAddGroup
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.OrderedIntervalFamily
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOAddition
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOAdditionFiber
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOSumset
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.SeparatedPieceFamily
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.SmallClosedSubspace
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Tests.CantorBendixson
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Tests.Refinement
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module.ArchimedeanBallSplitting
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module.ConvexQuotientSplitting
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module.Tests
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Ring.Hom.OfInjectiveComp
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.AssociatedGraded
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.AssociatedGradedValuation
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.DegreeAssociatedGraded
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.DegreeAssociatedGradedQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.FiltrationDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.QuotientDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.RV
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Residue
LeanPool.ConwayRefinement.ConwayRefinement.Data.Multiset.Tests.SelectionComplexity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.DegreeResidue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.DegreeValuation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Tests.SupportSupremumMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.DegreeTwo
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.DegreeTwoExample
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.Factorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.FactorizationClassification
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.TranslatedSpanFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.TranslatedTruncationSpan
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.ClassIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.CoefficientRandom
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.GradedIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.HereditaryIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.IndependenceWindow
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.MainTheorem
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.NonPrincipalIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.NormalFormBlocks
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.PrincipalIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.Random
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.RandomBlocks
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.ReducibleSpan
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.SuccessorStep
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.SupportRandom
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.TruncationIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.Factorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.FiniteSupportFactorUniqueness
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.MaximalFiniteMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.MaximalFiniteSupportDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalDivisibilityReflection
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalMaximalDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalScalarRedistribution
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalSubringFraction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalSubringPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.SeriesMaximalFiniteSupportDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.SeriesPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.AlmostIrreducible
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.AlmostIrreducibleFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.DegreeTwo
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.GermLikeFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.GradedDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.InfiniteSupportFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.MaximalFiniteSupportDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.NormalizedHPart
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.NormalizedHPartMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.PrincipalMaximalFiniteSupportDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.SectionSixFour
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.SeriesMaximalFiniteSupportDivisor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Additive
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.AlgebraicIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Boundary
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Cancellation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.CantorBendixsonRankLevels
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.CantorBendixsonValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.CantorBendixsonValueMultiplicativity
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.CofactorInduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Convolution
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Derivation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.DerivationIdeal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.DerivationSet
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Derivative
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Germ
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.GlobalCofactors
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Graded
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LeadingCoefficient
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Leibniz
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LiftFamily
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Lifts
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LimitOrdinalEvaluation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LimitOrdinalRelationAtCutoff
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LinearMaximal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LowerTruncationDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Multiplication
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Obligations
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.OrderedIntervalCantorBendixson
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.PartialDerivativeIndices
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.PartialDerivativesAtLimitOrdinal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Power
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.PrincipalSeries
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Scalar
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.ScalarLeadingCoefficientAtLimitOrdinal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.SeparatedPieceCantorBendixson
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.SuccessorLeibniz
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.SyzygyIntegration
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TranslatedTruncationInterpolation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TranslatedTruncationInterpolationOnSets
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Truncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TruncationExpansion
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TruncationPolynomial
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.CardinalGermRefinement
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.CardinalTruncationClosedClass
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.ClosedClassRefinementTransport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.CompleteGermRefinement
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.ConvexRestrictionFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.FiniteGermError
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.LimitTailRefinement
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.SupportClassFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.SupportClassRefinement
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.TruncationIntegerPartFractionField
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.Assumptions
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.Basic
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.CardinalPrimalityTransfer
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.CardinalProposition922
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.ClassTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.FiniteClassReduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.IntegerPartSplitting
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.PrimalityTransfer
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.Reduced
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.ReducedCharacterization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.ReducedDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.Reduction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.SplitTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.TruncationDivisibility
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Tests.TruncationPrimality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.BaseChange
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.CantorBendixsonGrading
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.CantorBendixsonRank
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.CantorBendixsonRepresentatives
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.CombinedCofactors
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAt
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAtInjective
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivationIdeal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.IdealFromTruncations
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.InductionOverDegrees
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LeadingCoefficient
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Lifts
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LimitOrdinalRelationAtCutoff
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LinearMaximal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LowDegreeParts
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LoweringDerivation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.OmegaSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.OrdinalValueCutoffs
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PartialDerivativeIndices
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Partials
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Pieces
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Polynomiality
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PrincipalGraded
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PrincipalIdealGE
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PrincipalRepresentatives
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.ProductCondition
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.ProductTruncation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.ProductValues
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.RealPartials
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SeriesTruncations
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Shift
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SuccessorLeibniz
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SuccessorSupportBound
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SumAlongCutoffs
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SupportLoweringPieces
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.Syzygy
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.TruncationExpansion
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.TruncationPolynomial
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.TruncationsIdeal
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.UnboundedTruncations
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.MainLemma
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.OrdinalValueDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ResidualPoint
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.BerarducciPrimitives
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.ComplexityDecrease
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.Convolution
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.ConvolutionList
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.ConvolutionRemainder
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.CriticalPoint
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.OrdinalValueFinalSegment
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.OrdinalValueSubmultiplicative
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalComponent
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalComponentDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalComponentTensor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalSubring
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalSubringFiniteSupport
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalSubringFraction
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalSubringTensor
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalValue
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.ResidualPoint
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.SectionSixThree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.Tests.GCDMonoid
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PolynomialAlgebra.Tests.PolynomialRing
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus.Pointwise
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.Germ.LinearMap
LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.Tests.FunAtZeroMinus
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.GeneralFactorization
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.NaturalPrincipal
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.OrderedUnion
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.OrdinalFactors
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.OrdinalFinitePart
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.OrdinalSuccessorFactorization
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.SetOrderType
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Tests.Sumset
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.Tests.Game
LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.Tests.GameOperations
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.DegreeTwoPrime
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.DegreeTwoPrimeProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.FiniteDegreeFamily
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.FiniteDegreeFamilyProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmegaOmegaBoundary
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmegaOmegaBoundaryProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmegaRoots
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmegaRootsProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmnificFactorization
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OmnificFactorizationProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OneRowPrime
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.OneRowPrimeProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.ConwayNormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.ConwayRefinementConsequences
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.DegreeTwoExample
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.FinitePowerFamily
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.FinitePowerFamilyProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OmegaOmegaBoundary
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OmnificFactorizationProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OmnificFiniteDegree
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OmnificIntegers
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OneRowExample
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.PrincipalRVAlgebraicIndependenceProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.DegreeTwoPrime
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.DegreeTwoPrimeProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.HahnIntegerPartRefinementCriterion
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.HahnIntegerPartRefinementCriterionProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.NegativeMonomialRoots
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.NegativeMonomialRootsProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.ArchimedeanQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.CompleteHahnGermProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.ConvexQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.ConvexQuotientSplitting
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.ConwayRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.ConwayRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.GermPolynomialRingProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.HahnIntegerPartRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.HahnLimitTailQuotient
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.HahnSeriesGCDProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.HahnSeriesPolynomialRingProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.InlineConwayRefinementProof
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.InlineSurreal
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.OrderedAddGroup
LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.SeriesConsequences
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.CardinalIntegerPart
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.DegreeTransfer
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.Full
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.Multiplication
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.NormalFormAdd
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Tests.NormalFormMul
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.FiniteClasses
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.IrreducibleOmnificIntegers
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.OmnificIntegers
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.OrdinaryIntegers
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.ZFC
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Refinement.ConwayRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.Basic
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.ConwayRefinement
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.DegreeTwoOzPrime
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.FiniteClasses
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Tests.ZFC
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Tests.Cuts
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Tests.Identification
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Tests.NormalForm
LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Tests.Properness
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.Tests.CantorBendixsonConvexCover
LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.Tests.PWOAddition
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module.Tests.ArchimedeanBallSplitting
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures.PolynomialAssociatedGraded
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures.PolynomialDegree
LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures.PolynomialQuotientDegree
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.DegreeTwo.FactorizationClassification
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.DegreeTwo.TranslatedSpanFactorization
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Tests.DegreeTwo.TranslatedTruncationSpan
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.BaseChange
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.CutoffConvolution
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.DerivAt
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.FinitePowerFamily
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.LoweringDerivation
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.OmegaOmegaBoundary
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.PrincipalGraded
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.PrincipalIdealGE
LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.AlgebraicIndependence.SuccessorLeibniz

Imported by