Glossary: C

Definitions in this project whose names start with C. The whole glossary has the other sections.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

C def

def C (n : ℕ) : Set (ℤ × ℤ × ℤ) · CongruentNumber.C

C def

C ε is the least C such that, for all primes p, every residue modulo p is the sum of at most C elements of {n⁻¹ : 1 ≤ n ≤ p^ε} (or 0 if no such C exists). · Erdos1180.C

C def

The infimum of all valid exponents [Gr26]. · Green19.C

c abbrev

abbrev c (n : Name) : Expr · c

c def

The growth exponent c(p, q) = liminf_{n → ∞} (log H(n)) / (log n). · Erdos667.c

c def

The infimum of $\|f \ast f\|_p$ over unit-interval densities. · Green35.c

c def

$c(n)$ starts with $(1, -3, -7, 17)$ and satisfies the same recurrence as a · OeisA100434.c

c def

The $n$-th coefficient of the square of the ordinary generating function $A(x)^2$. · OeisA185895.c

C1a def

Tao's Optimization constant 1a / An autocorrelation constant related to Sidon sets: The largest constant $C$ such that $$\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t - x) f(x)\,dx \ge C \left(\int_{-1/4}^{1/4} f(x)\,dx\right)^2$$ … · Constant1a.C1a

C6 abbrev

C6: Cycle graph on 6 vertices. · WrittenOnTheWallII.Test.C6

Candidate structure

structure Candidate (n : ℕ) · BusyBeaver.Candidate

canonicalHeight def

The canonical height lim_n 4⁻ⁿhₓ(2ⁿP) in terms of the logarithmic height hₓ. · WeierstrassCurve.Affine.Point.canonicalHeight

cantorPoint def

The point of $C(\alpha)$ with digit sequence $\varepsilon$, that is $(\alpha - 1) \sum_{k \ge 1} \varepsilon_k \alpha^{-k}$. · Bugeaud61.cantorPoint

cardinalPartitionRel def

cardinalPartitionRel μ r γ ν asserts the multicolor $r$-uniform partition relation $$\mu \to (\nu_\alpha)_{\alpha < \gamma}^r.$$ · Combinatorics.cardinalPartitionRel

cardIsSumThreePowerBelow def

The number of integers $\leq x$ which are the sum of three $k$th powers. · Erdos325.cardIsSumThreePowerBelow

cardSet def

The set of $N$ such that any $N$ points in the plane, no three on a line, contain a convex $n$-gon. · Erdos107.cardSet

cardSet def

The set of cardinalities m such that every m-point subset of ℝ^d contains an n-point subset with all pairwise distances distinct. · Erdos1088.cardSet

carmichaelCounting def

Let $C(x)$ count the number of Carmichael numbers in the interval $[1,x]$. · Erdos1057.carmichaelCounting

CarmichaelTotientFor def

Natural number $n$ for which there exists a $m ≠ n$ with $φ(m) = φ(n)$ · CarmichaelTotient.CarmichaelTotientFor

caroWei def

The exact rational Caro--Wei sum. · WrittenOnTheWallII.GraphConjecture430a.caroWei

caRule167 def

The rule function for Rule 167. Inputs must be 0 or 1. · OeisA267581.caRule167

caState def

The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. The initial condition is a single ON cell at $x=0$. $C(t, x)$ is structurally recursive on $t$. · OeisA267581.caState

catalanConstant def

Catalan's constant $$G = \sum_{n=0}^∞ (-1)^n / (2n + 1)^2 \approx 0.91596$$ · catalanConstant

catalanMersenne def

The Catalan-Mersenne numbers, defined recursively by $c_0 = 2$ and $c_{n+1} = 2^{c_n} - 1$. · Mersenne.catalanMersenne

catalanReciprocalSum def

The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers. · OeisA108.catalanReciprocalSum

Category inductive

A type to capture the various types of statements that appear in our Lean files. · ProblemAttributes.Category

categoryAnswerLinter def

The linter checking that solved statements do not use answer(sorry). · CategoryAnswerLinter.categoryAnswerLinter

categoryDocstringLinter def

The linter checking for docstrings on research statements. · CategoryDocstringLinter.categoryDocstringLinter

categoryLinter def

The problem category linter checks that every theorem/lemma/example has been given a problem category attribute. · CategoryLinter.categoryLinter

categoryNeedsAnswer def

Whether the given category is research solved. · CategoryAnswerLinter.categoryNeedsAnswer

categoryNeedsDocstring def

Whether the given category requires a docstring. · CategoryDocstringLinter.categoryNeedsDocstring

CategoryTag structure

TODO(lezeau): do we eventually want to account for the problem's source? · ProblemAttributes.CategoryTag

CayleyBall def

The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating set S. · GromovPolynomialGrowth.CayleyBall

cayleyGraph def

The (undirected) Cayley graph of a group $G$ with respect to a generating set $S$. Two elements $g, h \in G$ are adjacent iff $g \neq h$ and $g^{-1} h \in S$ or $h^{-1} g \in S$. · BabaiSeressConjectures.cayleyGraph

CDSColorable def

A finite graph is CDS-colorable if it has a proper coloring by natural numbers such that for all k > 0, the number of vertices with color < k equals the maximum size of the union of k independent sets. · SimpleGraph.CDSColorable

Cell def

def YoungDiagram.Cell (μ : YoungDiagram) : Type · YoungDiagram.Cell

centerAction def

The centre of the universal enveloping algebra acting on the C^∞ functions on GL n ℝ. Restricting envelopingAction to the centre, this is the action condition (c) in the definition of an automorphic form refers to. · Matrix.GeneralLinearGroup.centerAction

centerColumn def

The center column of Rule 30: the value of the single central cell (position $0$) at time $t$. · Rule30.centerColumn

centerFinset def

The center of a finite graph. · WrittenOnTheWallII.GraphConjecture430a.centerFinset

centerOn def

The centre of a valuation subring 𝒪 of F on a k-subalgebra A of F contained in 𝒪: the prime ideal 𝔪_𝒪 ∩ A of A. · ValuationSubring.centerOn

centerUniversalEnveloping abbrev

The centre of the universal enveloping algebra of the complexified Lie algebra of GL n ℝ. This is the algebra acting in condition (c) in the definition of an automorphic form. · Matrix.GeneralLinearGroup.centerUniversalEnveloping

cfEntropy def

The entropy $E(\xi)$ of the continued fraction expansion of $\xi$. · Real.cfEntropy

Cfg structure

The configuration state of a Turing machine during operation consists of a label (machine state), and a tape. The tape is represented in the form (a, L, R), meaning the tape looks like L.rev ++ [a] ++ R with the machine currently … · Turing.BusyBeaver.Cfg

checkAssumptionsStillOpen def

Warns when a hypothesis assumed by a conditional formal_proof has since been proved, so the proof may no longer be conditional on it. · FormalProofLinter.checkAssumptionsStillOpen

checkDecl def

Checks a declaration command for stubs, placeholder definitions, and axioms. · StubLinter.checkDecl

checkExactlyOneCategory def

Warns unless a carries exactly one category attribute. Returns whether it does, so the caller can go on to the checks that need one. stx is only used to place a warning when the modifiers carry no attribute list to point at. · CategoryLinter.checkExactlyOneCategory

checkExistsArrow def

Checks if an expression contains the pattern ∃ x, P x → Q. · ExistsImplicationLinter.checkExistsArrow

checkImports def

Checks a parsed header against the Formal Conjectures import rules. meta imports are exempt from the rules on direct Mathlib and FormalConjecturesForMathlib imports. · ImportLinter.checkImports

checkNotOpenIfSorryFree def

Warns when a problem categorised as research open turns out to have a sorry-free proof. · CategoryLinter.checkNotOpenIfSorryFree

checkProofIsSorryIfFormalProof def

Warns when a statement with a formal_proof annotation has a proof that is not exactly sorry or by sorry, unless it is conditional. The main branch is a statement repository, so proofs should live in their own repository or branch. · FormalProofLinter.checkProofIsSorryIfFormalProof

chromaticCardinal def

The chromatic cardinal is the minimal number of colors need to color it. In contrast to chromaticNumber, which assigns ⊤ : ℕ∞ to all non-finitely colorable graphs, this definition returns a Cardinal and can therefore distinguish … · SimpleGraph.chromaticCardinal

chromaticCardinal def

The infimum of cardinalities of color types admitting a proper coloring. The value is zero when no proper coloring exists. · UniformHypergraph.chromaticCardinal

Circle def

A circle of a particular radius as a subset of the Euclidean plane. The radius is a nonnegative real, so that Circle r is always the disc of radius $r$. Not including border, so that circles that touch at the border are disjoint, but a … · SquarePacking.Circle

circleMax def

The maximum of $\lvert P(z)\rvert$ over the unit circle, for $P(z)=\sum_{1\leq k\leq n}a_kz^k$. · Erdos230.circleMax

circleSeven def

Regular 7-gon with unit side length, touching both axes in the first quadrant. · Erdos91.circleSeven

circumference def

circumference G is the length of the longest cycle in G. It is 0 when G is acyclic. · SimpleGraph.circumference

Claim def

The assertion asked about in Problem 521: almost surely R_n / log n → 2/π. · Erdos521.Claim

ClassesUpTo def

All classes (n, a) with 2 ≤ n ≤ x and a < n. · Erdos1188.ClassesUpTo

classicalRamsey def

The classical two-color Ramsey number R(k, l) = R(K_k, K_l). · SimpleGraph.classicalRamsey

classNumberOfDiscriminant def

The class number of the quadratic field with discriminant $d$. · OeisA38552.classNumberOfDiscriminant

claudeAlpogeHowell31 def

The elliptic curve over ℚ of rank at least 31 found by Claude, Levent Alpöge and Ava Howell in 2026. It has rank exactly 31 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer conjecture. · EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31

cliqueExtremalNumber def

The extremal number forbidding a complete uniform hypergraph. · Hypergraph.cliqueExtremalNumber

CliqueFree def

A labelling of the edges of the complete graph on V by ι is n-clique-free when no colour class contains an n-clique, that is, when it admits no monochromatic n-clique. · SimpleGraph.TopEdgeLabeling.CliqueFree

cliqueSizes def

The set of sizes of the cliques (maximal complete subgraphs) of G. · SimpleGraph.cliqueSizes

cliqueSizes def

The sizes of the finite maximal complete subgraphs. · UniformHypergraph.cliqueSizes

cliqueSubdivision def

The graph G_k: the bipartite graph between {y_1, …, y_k} (the elements of Fin k) and {z_1, …, z_{k choose 2}} (the two-element subsets of Fin k), each z being joined to the two elements of the corresponding pair. This is the … · Erdos1021.cliqueSubdivision

ClosedInvariantSubspace structure

ClosedInvariantSubspace T is the type of non-trivial (different from H and {0}) closed subspaces of a complex vector space H that are invariant under the action of linear map T. · InvariantSubspaceProblem.ClosedInvariantSubspace

closedLemniscate def

The closed unit lemniscate $\{z : \lvert f(z)\rvert \leq 1\}$ of a complex polynomial. · Erdos1046.closedLemniscate

clusterPrimeCount def

The counting function of cluster primes $\le n$. · Erdos17.clusterPrimeCount

cmJInvariants def

The thirteen rational CM $j$-invariants, corresponding respectively to the imaginary quadratic orders of discriminants $-3,-4,-7,-8,-11,-12,-16,-19,-27,-28,-43,-67,-163$. · SatoTateConjecture.cmJInvariants

cmJInvariants def

The thirteen rational CM $j$-invariants. · SerreUniformity.cmJInvariants

cochromaticNumber def

The cochromatic number of a graph is the minimal number of colors needed to color its vertices so that each color class induces either an independent set or a complete graph. This is ⊤ (infinity) iff G isn't cocolorable with finitely … · SimpleGraph.cochromaticNumber

Cocolorable def

G.Cocolorable n means that the vertices of G can be colored with n colors so that each color class induces either an independent set or a complete graph. · SimpleGraph.Cocolorable

coeff def

The $n$-th Taylor coefficient of $f$ at $0$, i.e. $b_n = f^{(n)}(0) / n!$. · GoodmanConjecture.coeff

cofactorThreshold def

The cofactor threshold $h(n)$, for every positive $n$, is the largest cofactor lower bound for $n$. · Erdos539.cofactorThreshold

CohnElkiesAdmissible def

Definition 2.1 from [CoEl03]: A function is admissible if it is continuous and both the function and its Fourier transform decay sufficiently fast. Continuity is essential: changing f at a single point leaves fHat f unchanged, so … · Green42.CohnElkiesAdmissible

CohnElkiesOptimal def

The statement that there exists a function in dimension d satisfying the Cohn-Elkies scheme which achieves the center density bound bound. · Green42.CohnElkiesOptimal

cohomology abbrev

The cohomology H^*(A, M) = ⨁ n, Ext^n_A(k, M) of the bialgebra A over k with coefficients in the A-module M. It is a graded module over cohomologyRing k A under the Yoneda product. · Bialgebra.cohomology

cohomologyRing abbrev

The cohomology ring H^*(A, k) = ⨁ n, Ext^n_A(k, k) of the bialgebra A over k, where k is the trivial A-module through the counit and Ext is taken in ModuleCat A. It is a graded k-algebra under the Yoneda product. · Bialgebra.cohomologyRing

collatzStep def

Consider the following operation on the natural numbers: If the number is even, divide it by two. If the number is odd, triple it and add one. · CollatzConjecture.collatzStep

collatzStep def

Single step of the Collatz mapping. · OeisA153330.collatzStep

collatzSteps def

Number of iterations required to turn $n$ into 1 in the Collatz process, or none if $n$ does not terminate. · OeisA153330.collatzSteps

Colorable def

K_n admits a (4, 5)-colouring with k colours. · Erdos136.Colorable

colourEdgeCount def

The number of edges of $K_n$ inside H that get colour b under the colouring c. · Erdos162.colourEdgeCount

columnIdeal def

The left ideal of Matrix n n R consisting of the matrices with entries in I which are supported on the j-th column. · Koethe.columnIdeal

combineFirst def

Merge a configuration on the first $m$ parties and a configuration on the remaining $n-m$ parties into a configuration on all $n$ parties. · OpenQuantumProblem35.combineFirst

ComesFromPrimeQuadruple def

A number $n$ comes from a prime quadruple $(p, p+2, p+6, p+8)$ if $n = p(p+8)$ for some prime $p$ where $p$, $p+2$, $p+6$, $p+8$ are all prime. · OeisA56777.ComesFromPrimeQuadruple

CommonDifferencesThreeTermAP def

Given a finite set of integers A (modelled as a Finset ℤ), the set CommonDifferencesThreeTermAP A consists of all integers d such that there is a non-trivial three-term arithmetic progression a, b, c ∈ A with b - a = d and `c - … · Erdos1097.CommonDifferencesThreeTermAP

commonPair def

The 3-uniform hypergraph on four vertices consisting of two triples sharing a pair, $\{0,1,2\}$ and $\{0,1,3\}$. · Erdos593.commonPair

comp def

The composition of two vector valued polynomial functions. · MvPolynomial.RegularFunction.comp

complexity def

The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication. E.g. 2 = 1 + 1, so complexity 2 = 2. · Mathoverflow75792.complexity

complexPeriod def

The complex period as an integral: $\Omega_{\mathbb{C}}(E) = \int_{E(\mathbb{C})} |\omega \wedge \bar\omega| = 4 \int_{\mathbb{C}} dA(x) / |\Psi_2^2(x)|$. Source: LMFDB knowl ec.period. · WeierstrassCurve.complexPeriod

complexPeriodIntegrand def

The density of $\Omega_{\mathbb{C}}$ on the $x$-line: $1 / |\Psi_2^2(x)|$. · WeierstrassCurve.complexPeriodIntegrand

componentsIn def

The connected components of a set s ⊆ ℂ, viewed as subsets of ℂ. · Erdos1047.componentsIn

Composite abbrev

abbrev Nat.Composite (n : ℕ) : Prop · Nat.Composite

computable_avg_dist def

Computable average distance as a rational. · SimpleGraph.computable_avg_dist

computable_dist def

Computable graph distance via BFS. Returns 0 if u = v or if v is unreachable from u. · SimpleGraph.computable_dist

computable_dom_num def

Computable domination number via powerset enumeration. · SimpleGraph.computable_dom_num

computable_eccent def

The eccentricity of a vertex u in a finite graph as a computable natural number: the maximum BFS distance (computable_dist) from u to any vertex. · SimpleGraph.computable_eccent

computable_ediam def

The diameter of a finite graph as a computable natural number: the maximum BFS distance (computable_dist) over all ordered pairs of vertices. · SimpleGraph.computable_ediam

computable_indep_num def

Computable independence number via powerset enumeration. · SimpleGraph.computable_indep_num

computable_radius def

The radius of a finite graph as a computable natural number: the minimum, over all vertices, of the computable eccentricity. · SimpleGraph.computable_radius

computable_szeged_aux def

Computable Szeged auxiliary: count vertices closer to u than v. · SimpleGraph.computable_szeged_aux

computable_szeged_index def

Computable Szeged index. · SimpleGraph.computable_szeged_index

computable_wiener def

Computable Wiener index: half the sum of all ordered pairwise distances. · SimpleGraph.computable_wiener

computableDistMin def

A computable version of distMin for a Finset of vertices. · SimpleGraph.computableDistMin

computableLargestInducedBipartiteSubgraphSize def

Computable largest induced bipartite subgraph size via powerset enumeration. · SimpleGraph.computableLargestInducedBipartiteSubgraphSize

computableSaturationNumber def

Computable saturation number via powerset enumeration over the edge set. · SimpleGraph.computableSaturationNumber

concatenate def

Concatenate $x$ followed by $y$ in base 10. · OeisA70823.concatenate

concatenateNats def

Concatenates two natural numbers $a$ and $b$ base 10. · OeisA53067.concatenateNats

concatenateNats def

Concatenates two natural numbers $a$ and $b$ base 10. · OeisA67599.concatenateNats

concatNum def

Concatenation of numbers $n, n-1, \dots, n-k$. · OeisA87571.concatNum

Condition def

Given a polynomial p with rational coefficients, the predicate that if p takes integer values at all integers, the leading coefficient is positive and there exists no $d≥2$ with $d ∣ p(n)$ for all $n≥1$, then for all sufficiently large … · Erdos283.Condition

Condition def

Numbers $k$ such that the base $b$ expansion of $k$ for each $b = 3..k-1$ never contains more than two distinct digits. · OeisA306424.Condition

Config abbrev

A computational-basis configuration of $n$ parties with local dimension $d$. · OpenQuantumProblem35.Config

Configuration structure

A configuration of rectangles of sides 1 / (n + 1) and 1 / (n + 2). · Mathoverflow34145.Configuration

configurationExtremalNumber def

The extremal number forbidding e edges on v vertices (not necessarily induced). · Hypergraph.configurationExtremalNumber

CongruenceClass abbrev

A congruence class (n, a) represents a (mod n). · Erdos1188.CongruenceClass

Congruent def

Two finite sets of points are congruent if an isometry of the plane maps one onto the other. · Erdos103.Congruent

congruentNumber def

def congruentNumber (n : ℕ) : Prop · CongruentNumber.congruentNumber

Conj def

Conj α β is the conjunction α ∧ β. We define α & β as ~(α ~> ~β) for simplicity. · Arxiv.«1308.0994».Conj

conjClassCard def

The cardinality of the conjugacy class c. · ConjugacyClassSizes.conjClassCard

conjecture309Statement def

The universal inequality proposed in WOWII Conjecture 309. The Option-valued minimum makes the statement vacuous for complete graphs, whose complements have no edge; this totalization does not affect the counterexample. · WrittenOnTheWallII.GraphConjecture309.conjecture309Statement

ConjectureFor def

The predicate that the generalized Poincaré conjecture holds in dimension $n$, i.e. that any $n$-dimensional manifold that is homotopy equivalent to the sphere is in fact homeomorphic to the sphere. · PoincareConjecture.ConjectureFor

connectedDominationNumber def

The connected domination number of G. · SimpleGraph.connectedDominationNumber

coNP def

The class coNP is the set of decision problems whose complements are in NP. · ComplexityTheory.coNP

consecutivePrimeArithmeticProgressions def

The set of arithmetic progressions of consecutive primes of length $k$. · Erdos141.consecutivePrimeArithmeticProgressions

consecutivePrimesFrom def

consecutivePrimesFrom p k gives the set of k + 1 consecutive primes that are at least p in size. If p is prime then this is the set of k + 1 consecutive primes p, p_1, ..., p_k · Erdos786.consecutivePrimesFrom

ConsecutiveSumFree def

A finite set of naturals $A=\{a_1<\cdots<a_t\}$ is consecutive-sum-free if it has no solutions to $a_i+a_{i+1}+\cdots+a_j\in A$ with $i<j$; equivalently, whenever an interval $[m,n]$ contains at least two elements of $A$, the sum of the … · Erdos867.ConsecutiveSumFree

consecutiveSums def

The set of consecutive sums of a permutation p of {1,…,n}, where position k holds the value p k + 1: the sums ∑_{u ≤ k ≤ v} (p k + 1). · Erdos34.consecutiveSums

constantCompletion def

The completion function for constant-support states reduced to one party. · OpenQuantumProblem35.constantCompletion

constantConfig def

The constant configuration with value $a$. · OpenQuantumProblem35.constantConfig

constantsCharacter def

The character by which the centre of the enveloping algebra acts on the constant functions: z • 1 = constantsCharacter n z • 1. Its kernel is an ideal of finite codimension annihilating the constants, which gives condition (c) for … · Matrix.GeneralLinearGroup.constantsCharacter

contains_early_args def

Helper to check for arguments (h : True) · AnswerLinter.contains_early_args

ContainsAbelianSquare def

A string S contains an abelian square if it has two consecutive nonempty blocks x and y such that y is a permutation of x. · Erdos231.ContainsAbelianSquare

ContainsAP def

A set A contains an arithmetic progression of length k with difference d. · Set.ContainsAP

ContainsCompleteHypergraph def

A copy of the complete r-uniform hypergraph on k vertices. · Finset.ContainsCompleteHypergraph

ContainsCompletePartiteHypergraph def

A complete t-partite t-uniform hypergraph with r vertices in each part. · Finset.ContainsCompletePartiteHypergraph

containsLatex def

def containsLatex (s : String) : Bool · LatexDocstringLinter.containsLatex

containsLegacyUrlLink def

def containsLegacyUrlLink (s : String) : Bool · LatexDocstringLinter.containsLegacyUrlLink

ContainsMonoAPofLength def

def ContainsMonoAPofLength {κ : Type} [Finite κ] {M : Set α} (coloring : M → κ) (k : ℕ) : Prop · ContainsMonoAPofLength

containsSorry def

Whether stx contains a sorry anywhere. · CategoryAnswerLinter.containsSorry

ContainsSubgraph def

Some m vertices span at least k edges. · Finset.ContainsSubgraph

continuedFractionDenominator def

Helper function for a, which computes the denominator $R_k(n)$ of the continued fraction expression. For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: $$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ The base case is $R_{n-1}(n) = (n-1) - … · OeisA363347.continuedFractionDenominator

continuedFractionDenominator def

Recursive helper computing the continued fraction denominator $R_k(n)$ for $2 \le k \le n-1$, where $R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$ with base case $R_{n-1}(n) = (n-1) - \frac{n}{n+4}$. · OeisA372761.continuedFractionDenominator

ConvexIndep def

ConvexIndep S means that S consists of extremal points of its convex hull, i.e., the point set encloses a convex shape. Also known as a "convex-independent set". · EuclideanGeometry.ConvexIndep

convexUnitDistanceCounts def

The set of all possible numbers of unit distances determined by the vertices of a convex $n$-gon. · Erdos96.convexUnitDistanceCounts

Conway9 abbrev

The box product of two triangles is an example with 9 vertices satisfying the condition. (This graph is the complement of the one described in https://vimeo.com/109815595 and it is also isomorphic to it and to the Paley graph and the graph … · Conway99Graph.Conway9

Coprime def

A Finset of numbers is coprime, or relatively prime, if its gcd is 1. · Finset.Coprime

coprimeGraph def

The coprime graph on $\mathbb{N}$: two integers are joined by an edge if they are coprime. · Erdos883.coprimeGraph

coprimeIndices def

def coprimeIndices (r : ℕ) : Finset ℕ · OeisA211417.coprimeIndices

coprimeList def

The increasing list of integers < n that are coprime to n. · Erdos235.coprimeList

copyrightLinter def

The copyright linter ensures that every file has the right copyright header. · CopyrightLinter.copyrightLinter

correctCopyrightHeader def

The current correct copyright header. · CopyrightLinter.correctCopyrightHeader

correctCopyrightPrefix def

The part of the expected copyright before the year. · CopyrightLinter.correctCopyrightPrefix

correctCopyrightSuffix def

The part of the expected copyright after the year. · CopyrightLinter.correctCopyrightSuffix

coset def

def coset (c : CoveringSystem R) (i : c.ι) : Set R · CoveringSystem.coset

count def

For a strictly increasing sequence a of positive integers, count a x is the number of indices i with lcm(aᵢ, aᵢ₊₁) ≤ x. · Erdos440.count

countA def

Count of occurrences of value $v$ among $a(1), \dots, a(x)$. · OeisA182126.countA

CountablyMonolithicSpace class

A topological space is called ω-monolithic if the closure of every countable subspace is metrizable. · Homogeneous.CountablyMonolithicSpace

countDegreeK def

The number of vertices of degree k in G. · SimpleGraph.countDegreeK

countExceeding def

Count of numbers k in {1, ..., m} where k > (minFac k)^n. · OeisA87719.countExceeding

countGaps def

The number of gaps of size at most $c \cdot n / \varphi(n)$. · Erdos235.countGaps

countInducedC4 def

Count of induced C₄ subgraphs of G. We count ordered 4-tuples (a,b,c,d) of distinct vertices for which isInducedC4 G a b c d = true, then divide by 24 = 4!. · SimpleGraph.countInducedC4

counting def

The counting function $A(x)=\lvert A\cap [1,x]\rvert$. · Erdos785.counting

countingFn def

The counting function $\pi_A(N) = \#(A \cap [0, N])$ of the range $A$ of m. The outer Finset.range (N + 1) is harmless for a strictly increasing m, since then $n \le m_n$. · Bugeaud06.countingFn

countNotExceeding def

Count of numbers k in {1, ..., m} where k ≤ (minFac k)^n. · OeisA87719.countNotExceeding

countRefactorable def

countRefactorable x is the number of refactorable numbers $\le x$. · OeisA111291.countRefactorable

countRefactorableNat def

Helper function: number of refactorable numbers $\le m$. · OeisA111291.countRefactorableNat

CountSimultaneousPrimes def

CountSimultaneousPrimes S x counts the number of n ≤ x at which all polynomials in S attain a prime value. · BatemanHornConjecture.CountSimultaneousPrimes

countVsasmRows def

Number of ways to complete k remaining vertically symmetric ASM rows given the current column partial sums colSums. · OeisA109074.countVsasmRows

CoveredByC1 def

An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. · OeisA248802.CoveredByC1

CoveredByC2 def

An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, and m is not 1 mod 5, predicting a(k)=271. · OeisA248802.CoveredByC2

CoveredByC3 def

An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, and m is not 0 mod 5, predicting a(k)=523. · OeisA248802.CoveredByC3

coveringCopies def

The set of valid numbers of rotated copies of the pyjama set of width ε that cover the plane. · Green41.coveringCopies

coveringCount def

F(x): the number of minimal distinct covering systems all of whose moduli lie in [1, x]. · Erdos1188.coveringCount

CoveringSystem structure

A covering system of a semiring R is a finite set of cosets of non-zero ideals whose union covers the whole ring. In the case where R = ℤ, this corresponds to a choice of finitely many congruence relations such that every integer … · CoveringSystem

Covers def

Every integer satisfies some congruence of S. · Erdos1188.Covers

coversInitialInterval def

A list covers an initial interval of positive integers if the set of its elements is $\{1, 2, \dots, \max(l)\}$. · OeisA52709.coversInitialInterval

crossDistanceSet def

The set of distances $d(x, y)$ with $x \in A$ and $y \in B$. · Erdos661.crossDistanceSet

Cube structure

An axis-parallel homothetic copy of the standard n-cube. · Erdos769.Cube

cubeAdj def

Adjacency in the cube digraph: u is adjacent to v if v is obtained from u by bumping one coordinate. · ClaudesCycles.cubeAdj

cubes def

The set of perfect cubes in $\mathbb{N}$. · Erdos829.cubes

CuboidOne def

First Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the first Cuboid polynomial is irreducible. · EulerBrick.CuboidOne

CuboidOneFor def

Pairs of natural numbers for which the first Cuboid polynomial is irreducible. · EulerBrick.CuboidOneFor

CuboidThree def

Third Cuboid conjecture: For all positive, pairwise different coprime integers $a, b, c$ with $b * c ≠ a ^ 2$ and $a * c ≠ b ^ 2$, the polynomial of the third Cuboid polynomial is irreducible. · EulerBrick.CuboidThree

CuboidThreeFor def

Triplets of natural numbers for which the third Cuboid polynomial is irreducible. · EulerBrick.CuboidThreeFor

CuboidTwo def

Second Cuboid conjecture: For all positive coprime integers $a$, $b$ with $a ≠ b$, the polynomial of the second Cuboid polynomial is irreducible. · EulerBrick.CuboidTwo

CuboidTwoFor def

Pairs of natural numbers for which the second Cuboid polynomial is irreducible. · EulerBrick.CuboidTwoFor

cvetkovic def

Given a simple graph G with adjacency matrix A, this is the number n₀ + min n₊ n₋ where: - n₀ is the multiplicity of zero as an eigenvalue of A - n₊ is the number of positive eigenvalues of A (counting multiplicities) - n₋ … · SimpleGraph.cvetkovic

cyc def

The number of cyclic subgroups of a finite group G. · Arxiv.«2604.08040».cyc

Cycle structure

A cycle of G, carrying its basepoint. Bundling the basepoint makes the cycles of G into a type, so they can be collected into a Finset or a Multiset. · SimpleGraph.Cycle

cycleLengths def

G.cycleLengths is the set of lengths of the cycles in G. · SimpleGraph.cycleLengths

cycleRank def

The cycle rank of G (or cyclomatic number) is the minimum number of edges that must be removed to eliminate all cycles. · SimpleGraph.cycleRank

c₀ def

The constant $c_0 = \lim_{n \to \infty} u_n^{2^{-n}} = 1.5979102\ldots$ of [ElPl21, Corollary 3]. The sequence $u_n^{2^{-n}}$ is increasing and bounded by $2$ [ElPl21, Remark 3], so the limit is its supremum. This constant is the square of … · Erdos148.c₀

c₀ def

The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$. With the 0-indexing of u, the $n$-th term $u_n^{1/2^n}$ of the defining sequence is (u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1)) at i = n - 1. · Erdos315.c₀

C₁ def

The lower bound constant $C_1 \approx 3.2578$ from [Po20]. · Green38.C₁

C₂ def

The upper bound constant $C_2 \approx 3.3177$ from [La79]. · Green38.C₂