Documentation
Formalizations
Search
return to top
source
Imports
Init
Formalizations.LinearAlgebra.PointwiseProductSpan
Formalizations.MeasureTheory.PappusGuldin
Formalizations.MeasureTheory.Torricelli
Formalizations.MusicTheory.AllPairsEvenness
Formalizations.MusicTheory.CRTCharacters
Formalizations.MusicTheory.CircleOfFifths
Formalizations.MusicTheory.ComplementEnergy
Formalizations.MusicTheory.CycleGraphSpectrum
Formalizations.MusicTheory.CyclicHuddling
Formalizations.MusicTheory.CyclicHuddlingClosedForm
Formalizations.MusicTheory.CyclicHuddlingGeometry
Formalizations.MusicTheory.DiatonicExtremality
Formalizations.MusicTheory.DiatonicScale
Formalizations.MusicTheory.ExtremalityConnections
Formalizations.MusicTheory.Fourier
Formalizations.MusicTheory.GeneralisedHexachord
Formalizations.MusicTheory.Huddling
Formalizations.MusicTheory.IntervalVector
Formalizations.MusicTheory.InversionDFT
Formalizations.MusicTheory.MTransform
Formalizations.MusicTheory.MaximalEvenness
Formalizations.MusicTheory.MelodicWord
Formalizations.MusicTheory.NeoRiemannian
Formalizations.MusicTheory.ParityA6
Formalizations.MusicTheory.SixThirty
Formalizations.MusicTheory.Temperament
Formalizations.MusicTheory.Tiling
Formalizations.MusicTheory.TonnetzCompleteness
Formalizations.MusicTheory.TonnetzSpectrum
Formalizations.MusicTheory.TranslationInvariantEnergy
Formalizations.MusicTheory.TritoneFixedFourier
Formalizations.MusicTheory.TritoneNormal
Formalizations.NumberTheory.DedekindSum
Formalizations.NumberTheory.FermatQuotient
Formalizations.NumberTheory.LegendreSieve
Formalizations.NumberTheory.OrderOfTwo
Formalizations.NumberTheory.UnitsArithmeticProgression
Formalizations.NumberTheory.Willans
Formalizations.NumberTheory.Wolstenholme
Formalizations.Probability.Kemeny
Formalizations.RepresentationTheory.G2Counts
Formalizations.RingTheory.KostantAlphabet
Formalizations.Algebra.Ring.Continuant
Formalizations.AlgebraicGeometry.PlaneCurve.Cotes
Formalizations.Analysis.InnerProductSpace.Hlawka
Formalizations.Analysis.Polynomial.EnestromKakeya
Formalizations.Analysis.Polynomial.McMullin
Formalizations.Analysis.TransformerAttention.CardyPDI
Formalizations.Analysis.TransformerAttention.CayleyMap
Formalizations.Analysis.TransformerAttention.CriticalExponents
Formalizations.Analysis.TransformerAttention.EntropyBound
Formalizations.Analysis.TransformerAttention.GammaMobius
Formalizations.Analysis.TransformerAttention.HeatCapacity
Formalizations.Analysis.TransformerAttention.MaxEnt
Formalizations.Analysis.TransformerAttention.Pade
Formalizations.Analysis.TransformerAttention.RGFlow
Formalizations.Analysis.TransformerAttention.ResidualJacobian
Formalizations.Combinatorics.Additive.AddClosedInterval
Formalizations.Combinatorics.Additive.DissociatedGreedy
Formalizations.Combinatorics.Choose.MiddleBinomialDensity
Formalizations.Combinatorics.Choose.MiddleBinomialDivisors
Formalizations.Combinatorics.Choose.Singmaster
Formalizations.Combinatorics.Configuration.BruckRyserChowla
Formalizations.Combinatorics.Enumerative.LocalMaxima
Formalizations.Combinatorics.Enumerative.PrimeCongruences
Formalizations.Combinatorics.Enumerative.Touchard
Formalizations.Combinatorics.Frieze.IntegerDominance
Formalizations.Combinatorics.Frieze.TwoSignChanges
Formalizations.Combinatorics.Hall.Tight
Formalizations.Combinatorics.LatinSquare.Terrace
Formalizations.Combinatorics.Matroid.Transversal
Formalizations.Combinatorics.Matroid.TransversalObstruction
Formalizations.Combinatorics.Permanent.Bregman
Formalizations.Combinatorics.SetFamily.Bondy
Formalizations.Combinatorics.SimpleGraph.JohnsonBound
Formalizations.Combinatorics.SimpleGraph.OrientedIncMatrix
Formalizations.Combinatorics.SimpleGraph.Panarboreal
Formalizations.Combinatorics.SimpleGraph.TripartiteTuran
Formalizations.Combinatorics.Words.SuffixPrefixAvoidance
Formalizations.Combinatorics.Zarankiewicz.LimitedAugmentedThree
Formalizations.FieldTheory.Finite.CartierOperator
Formalizations.FieldTheory.Finite.OddPowerVandermonde
Formalizations.FieldTheory.Finite.PolynomialCoprimality
Formalizations.Geometry.Euclidean.WolstenholmeInequality
Formalizations.Geometry.Projective.Pappus
Formalizations.GroupTheory.FiniteAbelian.OddCharacter
Formalizations.GroupTheory.GroupAction.BoundedMovement
Formalizations.GroupTheory.GroupAction.ChanGL
Formalizations.GroupTheory.GroupAction.DistinguishingNumber
Formalizations.GroupTheory.GroupAction.FanoOrder
Formalizations.GroupTheory.GroupAction.IBIS
Formalizations.GroupTheory.GroupAction.PolyaRedfield
Formalizations.GroupTheory.GroupAction.SectionRegular
Formalizations.GroupTheory.GroupAction.Separation
Formalizations.GroupTheory.GroupAction.SeparationDichotomy
Formalizations.LinearAlgebra.Eigenspace.JointInvolutions
Formalizations.LinearAlgebra.Matrix.Adjugate
Formalizations.LinearAlgebra.Matrix.CauchyBinet
Formalizations.LinearAlgebra.Matrix.FinTwo
Formalizations.LinearAlgebra.Matrix.FreeLocus
Formalizations.LinearAlgebra.Matrix.FreeLocusCertificate
Formalizations.LinearAlgebra.Matrix.Rank
Formalizations.LinearAlgebra.Matrix.SchurCommuting
Formalizations.LinearAlgebra.Matrix.WalkCount
Formalizations.MachineLearning.ReLU.MaxFive
Formalizations.NumberTheory.ArithmeticFunction.DivisorTotient
Formalizations.NumberTheory.ArithmeticFunction.OeisA063880
Formalizations.NumberTheory.ArithmeticFunction.Untouchable
Formalizations.NumberTheory.Cyclotomic.ParityBounds
Formalizations.NumberTheory.DirichletCharacter.AbelZero
Formalizations.NumberTheory.Euclid.Lame
Formalizations.NumberTheory.Fibonacci.FibLegendre
Formalizations.NumberTheory.Fibonacci.Pisano
Formalizations.NumberTheory.Fibonacci.SumDivisibility
Formalizations.NumberTheory.MahlerBasis.EvenFunctions
Formalizations.NumberTheory.MahlerBasis.FiniteMahlerBasis
Formalizations.NumberTheory.MahlerBasis.LogarithmChange
Formalizations.NumberTheory.MahlerBasis.ParityAndKernel
Formalizations.NumberTheory.MahlerBasis.RankProfile
Formalizations.NumberTheory.NumericalSemigroup.FamilyMoments
Formalizations.NumberTheory.NumericalSemigroup.FourMoments
Formalizations.NumberTheory.NumericalSemigroup.GapBound
Formalizations.NumberTheory.NumericalSemigroup.GenusBound
Formalizations.NumberTheory.NumericalSemigroup.GenusThree
Formalizations.NumberTheory.PrescribedMoments.Biquanimous
Formalizations.NumberTheory.PrescribedMoments.CubicModels
Formalizations.NumberTheory.PrescribedMoments.DegreeCount
Formalizations.NumberTheory.Residues.ConsecutiveQuadratic
Formalizations.NumberTheory.SymplecticCharacterOrders.Arithmetic
Formalizations.NumberTheory.SymplecticCharacterOrders.LinearCoefficient
Formalizations.NumberTheory.SymplecticCharacterOrders.Multipliers
Formalizations.NumberTheory.SymplecticCharacterOrders.Segments
Formalizations.NumberTheory.SymplecticCharacterOrders.SupportAndIndex
Formalizations.NumberTheory.WeightedCharacterSums.DigitCorollaries
Formalizations.NumberTheory.WeightedCharacterSums.DigitRecursion
Formalizations.NumberTheory.WeightedCharacterSums.NoZeros
Formalizations.NumberTheory.WeightedCharacterSums.SubsetSumsAndRows
Formalizations.NumberTheory.WeightedCharacterSums.WeightedHalfSum
Formalizations.NumberTheory.Zsqrtd.GaussianMoatLine
Formalizations.RepresentationTheory.OrbifoldAlphabet.SymplecticBuild
Formalizations.RepresentationTheory.Symplectic.ResidueCapacity
Formalizations.RingTheory.AffineSemigroup.OrbifoldProduct
Formalizations.RingTheory.DGH.Absorb
Formalizations.RingTheory.DGH.Basic
Formalizations.RingTheory.DGH.Epsilon0
Formalizations.RingTheory.DGH.Finite
Formalizations.RingTheory.DGH.FqLower
Formalizations.RingTheory.DGH.Hessenberg
Formalizations.RingTheory.DGH.JakobsOrder
Formalizations.RingTheory.Polynomial.CyclotomicMultiset
Formalizations.RingTheory.Polynomial.GaussianBinomial
Formalizations.RingTheory.PowerSeries.LogMul
Formalizations.Analysis.ODE.RungeKutta.GaussLegendreOrder
Formalizations.Analysis.ODE.RungeKutta.OrderConditions
Formalizations.Analysis.Polynomial.RealRoots.BudanFourier
Formalizations.Analysis.Polynomial.RealRoots.Descartes
Formalizations.Analysis.Polynomial.RealRoots.NewtonInequalities
Formalizations.Analysis.Polynomial.RealRoots.RealRooted
Formalizations.Analysis.Polynomial.RealRoots.Sturm
Formalizations.Analysis.SpecialFunctions.Airy.Basic
Formalizations.Analysis.SpecialFunctions.Airy.Perturbation
Formalizations.Analysis.SpecialFunctions.Airy.PowerSeries
Formalizations.Analysis.SpecialFunctions.Dilogarithm.Basic
Formalizations.Analysis.SpecialFunctions.Dilogarithm.CircleFloor
Formalizations.Analysis.SpecialFunctions.Dilogarithm.Clausen
Formalizations.Analysis.SpecialFunctions.Dilogarithm.ComplexBoundary
Formalizations.Analysis.SpecialFunctions.Dilogarithm.FiveTerm
Formalizations.Analysis.SpecialFunctions.Integrals.LogDivSelf
Formalizations.Analysis.SpecialFunctions.Polylog.AntipodalCounterexamples
Formalizations.Analysis.SpecialFunctions.Polylog.HausdorffFloor
Formalizations.Analysis.SpecialFunctions.Trigonometric.FejerJackson
Formalizations.Combinatorics.SimpleGraph.Coloring.DeBruijnErdos
Formalizations.Combinatorics.SimpleGraph.Ihara.Bass
Formalizations.Combinatorics.SimpleGraph.Ihara.BassCommRing
Formalizations.Combinatorics.SimpleGraph.Ihara.GapWindow
Formalizations.Combinatorics.SimpleGraph.Ihara.GodsilMoment
Formalizations.Combinatorics.SimpleGraph.Ihara.MomentAssembly
Formalizations.Combinatorics.SimpleGraph.Ihara.MomentBridge
Formalizations.Combinatorics.SimpleGraph.Ihara.NbVanishing
Formalizations.Combinatorics.SimpleGraph.Ihara.NbWalkCount
Formalizations.Combinatorics.SimpleGraph.Ihara.PathTreeLift
Formalizations.Combinatorics.SimpleGraph.Ihara.PowerSumGenfun
Formalizations.Combinatorics.SimpleGraph.Ihara.PowerSumLogDeriv
Formalizations.Combinatorics.SimpleGraph.Ihara.ResolventDiag
Formalizations.Combinatorics.SimpleGraph.Ihara.TraceFormula
Formalizations.Combinatorics.SimpleGraph.Ihara.TreeLikeWalks
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.Basic
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.Divisibility
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.ExpectedCharpoly
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.ForestComponents
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.ForestRealRooted
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.GodsilGutman
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.HeilmannLieb
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.HeilmannLiebBound
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.MatchingSum
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.PathTree
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.RamanujanBound
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.Signing
Formalizations.Combinatorics.SimpleGraph.MatchingPolynomial.TwoLift
Formalizations.Combinatorics.SimpleGraph.MatrixTree.Basic
Formalizations.Combinatorics.SimpleGraph.MatrixTree.Kirchhoff
Formalizations.Combinatorics.SimpleGraph.MatrixTree.SpanningTreeMinor
Formalizations.LinearAlgebra.Matrix.Charpoly.Jacobi
Formalizations.LinearAlgebra.Matrix.Rank.Kronecker
Formalizations.NumberTheory.NumberField.InvariantOrders.BiquadraticIdentities
Formalizations.NumberTheory.NumberField.InvariantOrders.BiquadraticModel
Formalizations.NumberTheory.NumberField.InvariantOrders.ConjugatePowers
Formalizations.NumberTheory.NumberField.InvariantOrders.CubicParity
Formalizations.NumberTheory.NumberField.InvariantOrders.CyclicPrimeBezout
Formalizations.NumberTheory.NumberField.InvariantOrders.Discriminant
Formalizations.NumberTheory.NumberField.InvariantOrders.IndexFormula
Formalizations.NumberTheory.NumberField.InvariantOrders.IndexLemmas
Formalizations.NumberTheory.NumberField.InvariantOrders.Saturation
Formalizations.NumberTheory.NumberField.InvariantOrders.TriangularBasis
Formalizations.Physics.Particles.GaugeHiggsUnification.AlignmentPolynomials
Formalizations.Physics.Particles.GaugeHiggsUnification.BlindCount
Formalizations.Physics.Particles.GaugeHiggsUnification.ChargeQuantization
Formalizations.Physics.Particles.GaugeHiggsUnification.CosetCensus
Formalizations.Physics.Particles.GaugeHiggsUnification.EffectivePotentialAlgebra
Formalizations.Physics.Particles.GaugeHiggsUnification.HiddenCentreBasis
Formalizations.Physics.Particles.GaugeHiggsUnification.InternalU1MixingNoGo
Formalizations.Physics.Particles.GaugeHiggsUnification.LinearResponseIdentities
Formalizations.Physics.Particles.GaugeHiggsUnification.NotchCentreCharge
Formalizations.Physics.Particles.GaugeHiggsUnification.NotchDecoupling
Formalizations.Physics.Particles.GaugeHiggsUnification.OddEighths
Formalizations.Physics.Particles.GaugeHiggsUnification.R60JointExistence
Formalizations.Physics.Particles.GaugeHiggsUnification.R60LocalizedAnomaly
Formalizations.Physics.Particles.GaugeHiggsUnification.SU7ColourParity
Formalizations.Physics.Particles.GaugeHiggsUnification.SU7QPhiSelection
Formalizations.Physics.Particles.GaugeHiggsUnification.SU7RealPairing
Formalizations.Physics.Particles.GaugeHiggsUnification.SU7WeightChannels
Formalizations.Physics.Particles.GaugeHiggsUnification.ScalarCPSource
Formalizations.Physics.Particles.GaugeHiggsUnification.TorusTwistBasis
Formalizations.Physics.Particles.GaugeHiggsUnification.TwoThreeIndependence
Formalizations.Physics.Particles.GaugeHiggsUnification.USp4WeightMoments
Formalizations.Physics.Particles.GaugeHiggsUnification.WallDeterminants
Formalizations.Physics.QuantumMechanics.SpeedLimit.AntipodeFloor
Formalizations.Physics.QuantumMechanics.SpeedLimit.ApproxSpeedLimits
Formalizations.Physics.QuantumMechanics.SpeedLimit.DominantPopulation
Formalizations.Physics.QuantumMechanics.SpeedLimit.ExchangeQuadrature
Formalizations.Physics.QuantumMechanics.SpeedLimit.FixedAxisSaturation
Formalizations.Physics.QuantumMechanics.SpeedLimit.GateEigenphases
Formalizations.Physics.QuantumMechanics.SpeedLimit.MandelstamTamm
Formalizations.Physics.QuantumMechanics.SpeedLimit.MargolusLevitin
Formalizations.Physics.QuantumMechanics.SpeedLimit.QuditEntangling
Formalizations.Physics.QuantumMechanics.SpeedLimit.QuditEntanglingShift
Formalizations.Physics.QuantumMechanics.SpeedLimit.RefinedCZBound
Formalizations.Physics.QuantumMechanics.SpeedLimit.SpectralArc
Formalizations.Physics.QuantumMechanics.SpeedLimit.TwoQubitEntangling
Formalizations.Physics.QuantumMechanics.SpeedLimit.ZetaStateFloor
Formalizations.Physics.QuantumMechanics.SpeedLimit.ZielinskiZych
Formalizations.Physics.Supergravity.AnomalyQuantization.U2Example
Formalizations.Probability.Distributions.Superstatistics.LaplaceMixture
Formalizations.Probability.Distributions.Superstatistics.StudentMixture
Formalizations.RingTheory.FreeField.ThreeAxes.ArrowInstances
Formalizations.RingTheory.FreeField.ThreeAxes.ArrowMatrix
Formalizations.RingTheory.FreeField.ThreeAxes.AtomCertificate
Formalizations.RingTheory.FreeField.ThreeAxes.Basic
Formalizations.RingTheory.FreeField.ThreeAxes.BinomialSizeFamily
Formalizations.RingTheory.FreeField.ThreeAxes.ChainPencilConditions
Formalizations.RingTheory.FreeField.ThreeAxes.Criterion
Formalizations.RingTheory.FreeField.ThreeAxes.DegenerateResidue
Formalizations.RingTheory.FreeField.ThreeAxes.ExactArc
Formalizations.RingTheory.FreeField.ThreeAxes.Extractors
Formalizations.RingTheory.FreeField.ThreeAxes.InverseIdentities
Formalizations.RingTheory.FreeField.ThreeAxes.ParabolicFamily
Formalizations.RingTheory.FreeField.ThreeAxes.PhiCompression
Formalizations.RingTheory.FreeField.ThreeAxes.QuaternionCurve
Formalizations.RingTheory.FreeField.ThreeAxes.QuaternionResidues
Formalizations.RingTheory.FreeField.ThreeAxes.QuaternionTheta
Formalizations.RingTheory.FreeField.ThreeAxes.SizeChainPencil
Formalizations.RingTheory.FreeField.ThreeAxes.TraceResidue
Formalizations.RingTheory.FreeField.ThreeAxes.WeightedTrinomials
Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Abelianization
Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Adams
Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Basic
Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Coproduct
Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Eulerian
Formalizations.RingTheory.Polynomial.Chebyshev.Docagne
Formalizations.RingTheory.Polynomial.CoefficientRing.Division
Formalizations.RingTheory.Polynomial.CoefficientRing.Operations
Formalizations.RingTheory.Polynomial.CoefficientRing.Quadratic
Formalizations.RingTheory.Polynomial.CoefficientRing.Recentering
Formalizations.RingTheory.Polynomial.CoefficientRing.Residues
Formalizations.RingTheory.Polynomial.CoefficientRing.StableFamilies
Formalizations.RingTheory.Polynomial.CoefficientRing.StableIntervals
Formalizations.RingTheory.Polynomial.Cyclotomic.Migotti
Formalizations.SetTheory.Ordinal.Gentzen.Acc
Formalizations.SetTheory.Ordinal.Gentzen.Ordinals
Formalizations.SetTheory.Ordinal.Gentzen.TwoPow
Formalizations.Analysis.Polynomial.RealRoots.VirtualRoots.Basic
Formalizations.Analysis.Polynomial.RealRoots.VirtualRoots.Count
Formalizations.Physics.Particles.StandardModel.AxionCouplings.SpinPeriod
Formalizations.Physics.Particles.StandardModel.SMEFT.AllOrdersSelfCouplings
Formalizations.Physics.Particles.StandardModel.SMEFT.HiggsSelfCouplings
Formalizations.Physics.Particles.StandardModel.SMEFT.TopEdgeCollapse
Imported by