Glossary: I

Definitions in this project whose names start with I. 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

i0 def

A canonical element of the type (1 : Ordinal).ToType. · Erdos1167.i0

id def

def id : RegularFunction k σ σ · MvPolynomial.RegularFunction.id

imageSet def

The set of rational numbers of the form P(n) + 1 / n where n is a natural number and P is a polynomial with rational coefficients. · Erdos351.imageSet

imbalance def

The imbalance of a finite set X under a colouring f, that is, $\left\lvert \sum_{x<y\in X} f(x,y)\right\rvert$. · Erdos1028.imbalance

importLinter def

The import linter ensures that: - Files in FormalConjectures do not import Mathlib, Mathlib.*, FormalConjecturesForMathlib, or FormalConjecturesForMathlib.* directly. - Files in FormalConjectures import FormalConjecturesUtil. … · ImportLinter.importLinter

ImportRef structure

An import of a parsed header, retaining its syntax node. · ImportLinter.ImportRef

indepDominationNumber def

def indepDominationNumber (G : SimpleGraph α) : ℕ · SimpleGraph.indepDominationNumber

indepNeighbors def

The same quantity as a real number. · SimpleGraph.indepNeighbors

indepNeighborsCard def

Independence number of the neighbourhood of v. · SimpleGraph.indepNeighborsCard

indepNumDeleteVertex def

The independence number of the subgraph induced on $V \setminus \{v\}$ (i.e., the graph $G - v$). · WrittenOnTheWallII.GraphConjecture101.indepNumDeleteVertex

indepNumK def

The maximum size of the union of k finite independent sets. · SimpleGraph.indepNumK

indepNumOn def

Maximum cardinality of an independent subset contained in B. · SimpleGraph.indepNumOn

indepSum def

The discrete convolution of two PMFs on $\mathbb{Z}$, representing the distribution of the sum of two independent random variables. · Green28.indepSum

IndexCond def

The index condition on $(j, k)$ from the conjecture: $0 < \min\{2,k\} \le j \le k$. Since j and k are natural numbers, $0 < \min\{2,k\}$ is equivalent to $1 \le k$. · OeisA108.IndexCond

indexPairs def

The unordered index pairs, represented uniquely by the orientation i < j. · Erdos959.indexPairs

indicatorOne def

A polymorphic indicator function 𝟙_A which is 1 on A and 0 outside. · Set.indicatorOne

indices def

The set of positive indices $n$ for which $a(n) = v$. · OeisA153330.indices

InfinitelyConnected def

We say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths. Note that graphs with at most one vertex are not classed as infinitely connected. · SimpleGraph.InfinitelyConnected

InfinitelyEdgeConnected def

A graph is infinitely edge-connected if to disconnect the graph requires deleting infinitely many edges. In other words, removing any finite set of edges leaves the graph connected. · Erdos1067.InfinitelyEdgeConnected

infiniteWord def

The infinite word w is the fixed point of the morphism starting from 'a'. We define it as the limit: w(i) is the i-th symbol, which stabilizes after sufficiently many iterations. · OeisA6697.infiniteWord

InGeneralPosition def

A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is in general position if no three are collinear and no four lie on a circle. · EuclideanGeometry.InGeneralPosition

init def

The initial configuration. · Turing.BusyBeaver.Machine.init

InitialVelocityCondition structure

Basic conditions on initial velocity field for the Navier-Stokes equations in $n$-dimensional space. · NavierStokes.InitialVelocityCondition

InitialVelocityConditionDecay structure

Initial velocity conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$. · NavierStokes.InitialVelocityConditionDecay

InitialVelocityConditionPeriodic structure

Initial velocity conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$. · NavierStokes.InitialVelocityConditionPeriodic

inner_sum def

The inner sum of the formula used in a: $$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ · OeisA258667.inner_sum

InsideUnit def

A cube is nondegenerate and contained in the closed unit cube. · Erdos769.Cube.InsideUnit

integerDetN def

The exceptional values of $n$ where $1/\det(M)$ is conjectured to be an integer. · OeisA60841.integerDetN

IntegerDistancePlaneGraph def

An integer distance graph in ℝ²: the same construction with 1 replaced by an arbitrary positive integer, so two distinct points are adjacent exactly when the distance between them is a positive whole number. · SimpleGraph.IntegerDistancePlaneGraph

integralAdeles def

The integral adeles Ẑ = ∏ᵥ ℤᵥ as a subring of the finite adeles of ℚ: the adeles that are integral at every place. · Matrix.GeneralLinearGroup.integralAdeles

integralAdelicSubgroup def

GL n Ẑ inside GL n 𝔸ᶠ[ℤ, ℚ]: the matrices whose entries, and whose inverse's entries, are integral adeles. It is a compact open subgroup of G(𝔸_f) (isOpen_integralAdelicSubgroup, isCompact_integralAdelicSubgroup), as condition … · Matrix.GeneralLinearGroup.integralAdelicSubgroup

integralDiophantine4Tuple def

The set of integral Diophantine 4-tuples. · DiophantineTuple.integralDiophantine4Tuple

integralMeansSpectrum def

$\beta_f(\tau) := \limsup_{r \to 1^-} \frac{\log \int_{-\pi}^{\pi} |f'(re^{i\theta})|^\tau \, d\theta}{|\log(1-r)|}$ · BrennanConjecture.integralMeansSpectrum

interleave def

The sequence ⌊a⌋, ⌊b⌋, ⌊γ * a⌋, ⌊γ * b⌋, ... ⌊γ ^ i * a⌋, ⌊γ ^ i * b⌋, ... · Erdos354.FloorMultiples.interleave

internalEdges def

Edges of G whose two endpoints lie in S. · SimpleGraph.internalEdges

InternallyDisjoint def

Two walks are internally disjoint if they share no vertices other than their endpoints. · SimpleGraph.InternallyDisjoint

Intersecting def

A family F of sets is Intersecting if each pair of members has nonempty intersection. · Chvatal.Intersecting

intersectionMultiplicity def

The intersection multiplicity of two modules M and N over a commutative ring R, $$\chi(M, N) = \sum_{i \ge 0} (-1)^i \ell_R(\operatorname{Tor}_i^R(M, N)).$$ Here Tor is CategoryTheory.Tor on ModuleCat R, the sum is a … · Module.intersectionMultiplicity

IntersectsOnlyAtZero def

$A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$. · Green38.IntersectsOnlyAtZero

IntervalNonTernarySets def

IntervalNonTernarySets N is the (fin)set of non ternary subsets of {1,...,N}. The advantage of defining it as below is that some proofs (e.g. that of F 3 = 2) become rfl. · Erdos168.IntervalNonTernarySets

intervalRepresentations def

Let $a$ be an infinite sequence of integers. `intervalRepresentations A n` is the set of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ where `u` and `v` are positive integers. · Erdos358.intervalRepresentations

intervalRepresentationsNonTrivial def

Let $a$ be an infinite sequence of integers. `intervalRepresentationsNonTrivial A n` is the set of solutions to $$n=\sum_{u\leq i\leq v}a_i$$ such that the sum has at least two terms. · Erdos358.intervalRepresentationsNonTrivial

intPartialDensity def

The two-sided partial natural density of a set of integers, counted inside the interval [-N, N]. · Set.intPartialDensity

InUnit def

Membership in the half-open unit cube [0,1)^n. · Erdos769.InUnit

invertSeqC def

The c sequence for the general INVERT transform conjecture. $c(1) = 1$, $c(k)=ab^(k-2)$ for $k \ge 2$. · OeisA108306.invertSeqC

invertSeqD def

The INVERT transform of the sequence c. · OeisA108306.invertSeqD

irregularPrimes def

The set of irregular primes. · RegularPrimes.irregularPrimes

Is45Coloring def

An edge colouring of K_n with k colours is a (4, 5)-colouring if the six edges of every copy of K_4 receive at least five distinct colours. · Erdos136.Is45Coloring

IsA038552 def

$k$ is maximal among squarefree numbers such that $\mathbb{Q}(\sqrt{-k})$ has class number $n$. This defines the $n$-th term of A038552. · OeisA38552.IsA038552

IsAbsoluteEulerPseudoprime def

A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$. · OeisA307865.IsAbsoluteEulerPseudoprime

IsAbsolutelyNormal def

A real number x is absolutely normal if it is normal in every integer base b ≥ 2. · NormalNumber.IsAbsolutelyNormal

IsAbsoluteNeighborhoodRetract class

A topological space X is an absolute neighborhood retract (ANR) if, whenever it is embedded as a closed subspace of a normal space Y, there exists a continuous retraction from some open neighborhood of X in Y onto X. · IsAbsoluteNeighborhoodRetract

IsAccumulationPoint def

A point x is an accumulation point of a sequence s_0, s_1, ... if any neighbourhood of x contains a point of the sequence distinct from x. · Equidistribution.IsAccumulationPoint

IsAddComplete def

A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A. · IsAddComplete

IsAddCompleteNatSeq' def

A sequence A is complete if every sufficiently large element of M is a sum of (not necessarily distinct) terms of A. · IsAddCompleteNatSeq'

IsAdditionChain def

An addition chain is a strictly increasing sequence $1 = a_0 < a_1 < \cdots < a_r$ in which every entry after the first is the sum of two (not necessarily distinct) earlier entries. · IsAdditionChain

IsAdditiveComplement def

A and B are additive complements if A + B contains all large integers. · IsAdditiveComplement

IsAdditiveComplementToPrimes def

A set $A \subseteq \mathbb{N}$ is an additive complement to the primes if every sufficiently large natural number can be written as $p + a$ for some prime $p$ and $a \in A$. · Erdos32.IsAdditiveComplementToPrimes

IsAddStronglyComplete def

A set A ⊆ M is complete if every sufficiently large element of M is a subset sum of A. · IsAddStronglyComplete

IsAddStronglyCompleteNatSeq def

A sequence A is strongly complete if fun m => A (n + m) is still complete for all n. · IsAddStronglyCompleteNatSeq

IsAdmissible def

The polynomials under consideration: those of the form $f(z)=\prod_{i=1}^n(z-z_i)$, for some $n\geq 1$, where $\lvert z_i\rvert\leq 1$ for all $i$. · Erdos1044.IsAdmissible

IsAdmissible def

An edge-budget function $g$ is admissible for $r$ if every graph $G$ with the property that every subgraph $H$ on $m$ vertices is the union of a graph with chromatic number $\leq r$ and a graph with $\leq g(m)$ edges has chromatic number … · Erdos1092.IsAdmissible

IsAdmissible def

A set A ⊆ {1, …, N} is admissible if it contains N and any two distinct elements of A have a common factor. · Erdos534.IsAdmissible

IsAdmissible def

We say that c is admissible if, for any finite set A such that every four-element subset B determines at least five positive differences, there exists a Sidon subset S of size at least c * A.ncard. The difference condition is … · Erdos757.IsAdmissible

IsAdmissible def

A has no solution to $at=b$ with $a,b\in A$ and the smallest prime factor of $t$ greater than $a$. · Erdos858.IsAdmissible

IsAdmissibleDomain structure

The domain hypotheses of Pompeiu's problem: $\Omega$ is bounded, open, connected (a "domain"), simply connected, has Lipschitz boundary, and for $N \ge 2$ the complement of its closure is connected. For $N = 1$, connectedness of … · PompeiuProblem.IsAdmissibleDomain

IsAdmissiblePrimeConstellation def

A prime constellation is said to be admissible if its elements do not form a complete set of residue classes with respect to any prime. · HardyLittlewood.IsAdmissiblePrimeConstellation

IsAME def

A state $\psi$ is absolutely maximally entangled. · OpenQuantumProblem35.IsAME

IsAmicable structure

We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$. · IsAmicable

IsAnySizeEquilateralTriangle def

An equilateral triangle of any positive side length in Euclidean d-space. · Erdos755.IsAnySizeEquilateralTriangle

IsAPAndPrimeProgressionOfLength def

The predicate that a set s is both an arithmetic progression of length l and a progression of l consecutive primes. · Erdos141.Set.IsAPAndPrimeProgressionOfLength

IsAPCover def

A contains an arithmetic progression of length k and common difference d for every d ∈ {1, …, N}. · Green37.IsAPCover

IsAPOfLength def

A list version of Set.IsAPOfLength. Useful when order preservation is required, for example when considering images under arbitrary functions. · List.IsAPOfLength

IsAPOfLength def

The predicate that a set s is an arithmetic progression of length l (possibly infinite). This predicate does not assert a specific value for the first term or the difference of the arithmetic progression. · Set.IsAPOfLength

IsAPOfLengthFree def

We say that a set s is free of arithmetic progressions of length l if s contains no non-trivial arithmetic progressions of length l. Written as Set.IsAPOfLengthFree s l. - · Set.IsAPOfLengthFree

IsAPOfLengthWith def

A list version of Set.IsAPOfLengthWith. Useful when order preservation is required, for example when considering images under arbitrary functions. · List.IsAPOfLengthWith

IsAPOfLengthWith def

A set $S$ is an arithmetic progression of length $l$ with first term $a$ and difference $d$ if $S = \{a, a + d, ..., a + (l - 1)d\}$, if $l$ if finite, else $S = {a, a + d, a + 2d, ...}. This can be written as s.IsAPOfLengthWith l a d, … · Set.IsAPOfLengthWith

isApOfNPrimes def

The initial term $p_0$ and common difference $d$ form an arithmetic progression of length $n$ consisting entirely of prime numbers with $d > 0$. · OeisA7918.isApOfNPrimes

IsApproximable def

x is approximable with respect to f if $$\left\lvert x-\frac{p}{q}\right\rvert < \frac{f(q)}{q}$$ has infinitely many solutions with $(p,q)=1$. · Erdos999.IsApproximable

IsArithInterSet def

Let $N \in\mathbb{N}$. We say that $\{A_1, ..., A_t\}\subseteq \mathcal{P}(\{1, \dots, N\})$ is an arithmetic intersection set if $A_i \cap A_j$ is a non-empty arithmetic progression for each $i \neq j$. · Erdos272.IsArithInterSet

isAsmLine def

A list of integers in {-1, 0, 1} is a valid alternating sign matrix row/column if all of its prefix sums lie in {0, 1} and its total sum is 1. · OeisA109074.isAsmLine

isAsmLineAux def

Checks that all prefix sums of xs starting from acc lie in {0, 1} and the final sum is 1. · OeisA109074.isAsmLineAux

IsAsymptoticMulBasis def

An asymptotic additive basis of some order. · Set.IsAsymptoticMulBasis

IsAsymptoticMulBasisOfOrder def

def IsAsymptoticMulBasisOfOrder (A : Set M) (n : ℕ) : Prop · Set.IsAsymptoticMulBasisOfOrder

IsAtom def

A set $A$ is an atom if it has positive measure and for all $B \subseteq A$ measurable, either $\mu(B) = 0$ or $\mu(B) = \mu(A)$. · Arxiv.id2303_01089.MeasureTheory.IsAtom

IsAtomLess class

A measure is atomless if it has no atoms. · Arxiv.id2303_01089.MeasureTheory.IsAtomLess

IsAttractingCycle def

We say that z : ℂ is part of an attracting cycle of period n of f : ℂ → ℂ if it is an n-periodic point (i.e. f^[n] z = z), f^[n] is differentiable at z, ‖deriv f^[n] z‖ is strictly less than one, and n > 0. · Mandelbrot.IsAttractingCycle

IsAutomatic def

A sequence a is k-automatic if its k-kernel is finite. By [Eil74] this is equivalent to a being generated by a deterministic finite automaton reading the base-k digits of the index. · AutomaticSequence.IsAutomatic

IsAutomaticInBase def

The base-b expansion of ξ is generated by a finite automaton, in the classical sense: its digit sequence is b-automatic. · AutomaticSequence.IsAutomaticInBase

IsAutomorphicForm structure

An automorphic form for (G, K) in the sense of Borel-Jacquet, with G = GL n / ℚ and K = O n ℝ: G(𝔸) is written as G(𝔸_f) × G(ℝ) = GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ, condition (a) is invariance under ratDiagonal n, the rational points … · Matrix.GeneralLinearGroup.IsAutomorphicForm

IsBalanced def

A is ε-balanced: $\lvert F_A(g)-2^{|A|}/N\rvert \leq \epsilon 2^{|A|}/N$ for all g. · Erdos1179.IsBalanced

IsBalanced def

We call a graph $D$-balanced (or $D$-almost-regular) if the maximum degree is at most $D$ times the minimum degree. · SimpleGraph.IsBalanced

IsBalancedAbove def

Every set H of at least k vertices contains more than $\alpha\binom{|H|}{2}$ edges of each colour under c. · Erdos162.IsBalancedAbove

IsBalancedBigCohenMacaulay structure

A balanced big Cohen-Macaulay module over a local ring R is an R-module M, not necessarily finitely generated, with m • M ≠ M and such that every system of parameters of R is a regular sequence on M. · Module.IsBalancedBigCohenMacaulay

IsBall def

Ω is a Euclidean ball: an open metric ball of positive radius. · PompeiuProblem.IsBall

IsBarkerSequence def

A Barker sequence has $\pm 1$ entries and nontrivial autocorrelations of magnitude at most one. · Arxiv.«2104.00502».IsBarkerSequence

IsBarrier def

IsBarrier f n means n is a barrier for the real-valued function f, i.e. (m : ℝ) + f m ≤ (n : ℝ) for all m < n. · Erdos413.IsBarrier

IsBasePalindrome def

A natural number $n$ is a base-$b$ palindrome if its base-$b$ digits read the same forwards and backwards. · OeisA77408.IsBasePalindrome

IsBehrend def

A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$. In other words, if the set of multiples has natural density $1$. · Erdos26.IsBehrend

IsBestNTerm def

S achieves the best n-term Egyptian underapproximation of x, i.e. egyptianSum S realises $R_n(x)$. · Erdos206.IsBestNTerm

IsBetrothed structure

Two natural numbers $m$ and $n$ are betrothed (or quasi-amicable) if $\sigma(m) = \sigma(n) = m + n + 1$, where $\sigma$ is the sum-of-divisors function. Equivalently, the sum of the proper divisors of $m$ equals $n + 1$, and the sum … · BetrothedNumbers.IsBetrothed

IsBeurlingPrimes def

A sequence of real numbers 1 < a 0 < a 1 < ... is called a set of Beurling prime numbers if it tends to infinity. · IsBeurlingPrimes

IsBiInvariant def

A relation on a group is bi-invariant if it is preserved by both left and right multiplication. · Kourovka.«1.35c».IsBiInvariant

IsBinarySidon def

A set of binary vectors is Sidon if its pairwise sums, taken coordinatewise in ℕ, determine the unordered pair of summands. · Green31.IsBinarySidon

IsBipartition def

IsBipartition G X Y means that X and Y form a bipartition of the vertices of G. · Erdos1080.IsBipartition

IsBlockDesign def

Every t-set of ground vertices lies in exactly one block. · Finset.IsBlockDesign

IsBoundedSolution structure

The function $u : ℝ^n → ℝ$ is a bounded classical solution to $Δ u + u - u^3 = 0$. · DeGiorgi.IsBoundedSolution

IsBridgeless def

G is bridgeless if none of its edges is a bridge. · SimpleGraph.IsBridgeless

IsBroadlyAutomaticInBase def

The base-b expansion of ξ is generated by a finite automaton, in the broad sense: its digit sequence is k-automatic for some k ≥ 2, not necessarily for k = b. · AutomaticSequence.IsBroadlyAutomaticInBase

IsBuchi def

IsBuchi M asserts that whenever M consecutive values (x + n)² + a (for n = 0, …, M - 1) are all perfect squares, then a must be 0. · Buchi.IsBuchi

IsCancellative def

A finitely generated k-algebra A is cancellative if for all finitely generated k algebras B such that B[X] ≅ₖ A[X] we have B ≅ₖ A. · Arxiv.«2208.14736».IsCancellative

IsCarmichael def

A Carmichael number is a composite number n such that for all b ≥ 1, we have b^n ≡ b (mod n). · IsCarmichael

IsCarmichaelNumber def

Definition of a Carmichael number $n$: a composite number s.t. $b^{n-1} \equiv 1 \pmod n$ for all $b$ coprime to $n$. · OeisA309132.IsCarmichaelNumber

IsCcwConvexPolygon def

The statement that a sequence of points form a counter-clockwise convex polygon. · EuclideanGeometry.IsCcwConvexPolygon

IsCellularFamily def

A cellular family is a pairwise-disjoint collection of nonempty open sets. · WeaklyFirstCountable.IsCellularFamily

IsChordal def

A graph is chordal if it contains no induced cycle of length k ≥ 4. · SimpleGraph.IsChordal

IsClassNumberOne def

def IsClassNumberOne (d : ℤ) : Prop · ClassNumberProblem.IsClassNumberOne

IsCliqueEdgePartition def

P is a partition of the edges of G into cliques: each member of P is a clique of G with at least two vertices, and every edge of G is contained in exactly one member of P. · SimpleGraph.IsCliqueEdgePartition

IsClusterPrime def

A prime $p$ is a cluster prime if every even natural number $n \le p - 3$ can be written as a difference of two primes $q_1 - q_2$ with $q_1, q_2 \le p$. · Erdos17.IsClusterPrime

IsCoeffIntegralAdjointInvNat def

There exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$. · LamLitt.IsCoeffIntegralAdjointInvNat

IsCofactorLowerBound def

We say that $m$ is a cofactor lower bound for a given $n$ if, for every set $A$ of $n$ non-negative integers, there are at least $m$ cofactors $a / (a, b)$, where $a, b\in A$. · Erdos539.IsCofactorLowerBound

IsCoilInGraphOfLength def

A subgraph G' is a 'coil' of length k in graph G if it is an induced cycle of length k. · SnakeInBox.IsCoilInGraphOfLength

IsCompactFamily def

The family is compact: some single member already controls the family extremal number. · Erdos180.IsCompactFamily

IsCompactSequenceOn def

A sequence of natural numbers is compact on a set S if consecutive terms at distance 2 differ by 1 for all k ∈ S. · DegreeSequencesTriangleFree.IsCompactSequenceOn

IsComparableSet₂ def

A set of triples is $2$-comparable if any two distinct members of it are $2$-comparable. · Arxiv.«1609.08688».IsComparableSet₂

IsComparable₂ def

Two triples $t_1$ and $t_2$ are $2$-comparable if one of them is $2$-less than the other. · Arxiv.«1609.08688».IsComparable₂

IsComplete def

A ruler is complete (a perfect ruler) if its marks form a difference basis for $\{0, 1, \ldots, L\}$, i.e. every distance $k \le L$ is the difference of two marks. This is Finset.IsDifferenceBasis applied to the marks. · SparseRuler.IsComplete

IsCompleteHypergraphDecomposition def

Partition into complete r-graphs with either r or r+1 vertices. · Finset.IsCompleteHypergraphDecomposition

IsCompleteOn def

Every k-element subset of S is an edge. · UniformHypergraph.IsCompleteOn

IsComposite def

Helper definition for "composite number" · OeisA309132.IsComposite

IsConnectedDominating def

A set is a connected dominating set if it is dominating and induces a connected subgraph. · SimpleGraph.IsConnectedDominating

IsConnectedMap def

For topological spaces $X$ and $Y$ we say a function $f : X → Y$ is connected is it sends connected sets to connected sets. · Mathoverflow235893.IsConnectedMap

IsConsecutiveBlockSum def

IsConsecutiveBlockSum a k m means that $m$ equals the sum of at least two consecutive terms of the sequence $a$, using indices from $\{1, \ldots, k - 1\}$. That is, there exist $i, j$ with $1 \le i$, $i + 1 \le j$, $j \le k - 1$ such … · Erdos423.IsConsecutiveBlockSum

IsConstantConfig def

A configuration is constant if all coordinates agree. · OpenQuantumProblem35.IsConstantConfig

IsConvexPolygon def

The statement that a sequence of points form a convex polygon. · EuclideanGeometry.IsConvexPolygon

IsCoprimePowerfulAP4 def

The four numbers $a, a+d, a+2d, a+3d$ form a four-term arithmetic progression ($d > 0$) of pairwise coprime powerful numbers. · Erdos937.IsCoprimePowerfulAP4

IsCorner def

A corner in $A$ with common difference $d$ [FSS20]. · Green19.IsCorner

IsCountableUnionOfTriangleFree def

def IsCountableUnionOfTriangleFree {V : Type*} (G : SimpleGraph V) : Prop · Erdos595.IsCountableUnionOfTriangleFree

isCoveredBy def

The integer m is covered by one of the first k chosen congruence classes. · Erdos280.isCoveredBy

IsCoveredByResidues def

Given $x$ and $y$, can we cover the interval $[1, y]$ by residue classes $a_p \pmod p$ for each prime $p \le x$? · Green46.IsCoveredByResidues

IsCoveringFinset def

def IsCoveringFinset (n r : ℕ) (V : Finset (𝔽₂ n)) : Prop · Green40.IsCoveringFinset

IsCoveringSubspace def

$V$ is a covering subspace of $\mathbb{F}_2^n$ by $H(r)$ if $V + H(r) = \mathbb{F}_2^n$. · Green40.IsCoveringSubspace

IsCritical def

A graph G is k-critical (or vertex-critical) if its chromatic number is k, and deleting any single vertex reduces the chromatic number. · SimpleGraph.IsCritical

IsCriticalEdge def

An edge is critical if deleting it reduces the chromatic number. · SimpleGraph.IsCriticalEdge

IsCriticalEdges def

A set of edges is critical if deleting them reduces the chromatic number. · SimpleGraph.IsCriticalEdges

IsCriticalVertex def

A vertex is critical if deleting it reduces the chromatic number. · SimpleGraph.Subgraph.IsCriticalVertex

IsCriticalVerts def

A set of vertices is critical if deleting them reduces the chromatic number. · SimpleGraph.Subgraph.IsCriticalVerts

IsCrystalWithComponents def

An odd number $n$ is called a crystal if $n = ab$, with $a, b > 1$ and $B(a, b) ∈ ℕ$, where $B(a, b) := ((a + b)^2 + (a b + 1)^2) / (2 (a + 1) (b + 1))$. · Arxiv.«1601.03081».IsCrystalWithComponents

IsCube def

A cube is the image of $\lbrace 0, 1\rbrace^n$ under a linear automorphism. · Green26.IsCube

IsCut def

A two-part partition $\{A, B\}$ of $V$ is a cut if the convex hulls of $A$ and $B$ are disjoint. · Erdos97.IsCut

IsCutoff def

c is the minimal cutoff c(n): every k ≥ c is admissible, and (when c > 0) c - 1 is not. · Erdos769.IsCutoff

IsCuttable def

A triangle is n-cuttable if it can be decomposed into n congruent triangles. · Erdos633.IsCuttable

IsCycleCover def

C covers G: every edge of G lies on at least one cycle of C. · Arxiv.«2607.06396».IsCycleCover

IsCycleOrEdge def

A graph $H$ is a cycle or an edge if it is connected and 2-regular, or if it has exactly one edge. · Erdos184.IsCycleOrEdge

IsCyclicFamily def

No member of the family is acyclic. · Erdos180.IsCyclicFamily

IsDComplete def

A sequence is said to be $d$-complete if every large integer is the sum of distinct integers from the sequence, none of which divide any other. This particular case of $d$-completeness was conjectured by Erdős and Lewin [ErLe96], who … · Erdos123.IsDComplete

IsDecidable def

A theory T is decidable if the set of its consequences {φ | T ⊨ᵇ φ} is recursive: there is an algorithm which, given a sentence φ, decides whether φ holds in every model of T. · FirstOrder.Language.Theory.IsDecidable

IsDecimalPalindrome def

A natural number $m$ is a decimal palindrome if its base-$10$ digits read the same forwards and backwards. · OeisA83753.IsDecimalPalindrome

IsDecomposition def

D is a decomposition of G into edge-disjoint subgraphs: the edge sets of the members of D are pairwise disjoint and their union is the edge set of G. · SimpleGraph.IsDecomposition

IsDedekindZeta def

Z is a Dedekind zeta function of the number field K: it is holomorphic away from $s = 1$ and agrees with the Dedekind zeta series of K on $\operatorname{Re} s > 1$, where that series converges. Such a Z is uniquely determined on … · ArtinPrimitiveRootsConjecture.IsDedekindZeta

IsDefined def

A rational function $g$ is defined at a point $x_0$ if $g$ can be written as $p / q$ where $p, q$ are polynomials and $q(x_0) \neq 0$. · IsDefined

IsDegenerate def

H is r-degenerate when every induced subgraph has a vertex of degree at most r, that is, every nonempty vertex set contains a vertex with at most r neighbours inside it. · SimpleGraph.IsDegenerate

IsDelta₁ def

$\delta_1(n,m)$ is the density of the set of integers with exactly one divisor in $(n,m)$. · Erdos692.IsDelta₁

IsDescendingWave def

A $k$-term descending wave is a sequence $x_1<\cdots <x_k$ such that, for $1<j<k$, $x_j \geq \frac{x_{j+1}+x_{j-1}}{2}$. · Erdos781.IsDescendingWave

IsDiameter2Critical def

A graph is diameter-2-critical if it has diameter $2$ and removing any edge increases the diameter beyond $2$. · Erdos742.IsDiameter2Critical

IsDifferenceRecord def

A value $R$ is a difference record if there exists $n \ge 2$ such that $d(n) = R$ and $R$ is strictly larger than all previous differences $d(k)$ for $2 \le k < n$. · OeisA166944.IsDifferenceRecord

IsDiophantineTuple def

A finite set s is a Diophantine tuple if each element is nonzero and the product of any two distinct elements is one less than a perfect square. · DiophantineTuple.IsDiophantineTuple

IsDirectedHamiltonianCycle def

A permutation σ on vertices is a directed Hamiltonian cycle of a digraph with adjacency adj if every arc (v, σ v) is an edge, σ is a single cycle, and σ moves every vertex. · ClaudesCycles.IsDirectedHamiltonianCycle

IsDissociated def

We call $A\subset \mathbb{N}$ dissociated if $\sum_{n\in X}n\neq \sum_{m\in Y}m$ for all finite $X,Y\subset A$ with $X\neq Y$. · Set.IsDissociated

IsDistinctTotientRun def

IsDistinctTotientRun n K means that the values φ(n+1), φ(n+2), ..., φ(n+K) are all distinct. · Erdos1004.IsDistinctTotientRun

IsDistributionOfPhiRatio def

A function $f : \mathbb{R} \to \mathbb{R}$ is the asymptotic distribution function of the values of $\varphi(n)/n$ if for all $c \in [0, 1]$, the natural density of $\{n : \varphi(n) < cn\}$ exists and equals $f(c)$. · Erdos50.IsDistributionOfPhiRatio

IsDlabGroup def

$A$ is one of the six Dlab groups with slope group $H$. Each consists of the locally right $H$-linear order automorphisms $f$ with a condition at the ends. · Kourovka.«21.149».IsDlabGroup

IsDominating def

A set D is a dominating set for G if every vertex of G is either in D or adjacent to a vertex of D. · SimpleGraph.IsDominating

IsEdgeColouring def

IsEdgeColouring H c asserts that c : ι → SimpleGraph V is a partition of the edges of H: the colour classes cover H (H = ⨆ i, c i) and are pairwise disjoint. · SimpleGraph.IsEdgeColouring

IsEdgeCover def

A set of edges is an edge cover if every vertex is incident to some edge in it. · SimpleGraph.IsEdgeCover

IsEdgeDominating def

def IsEdgeDominating (G : SimpleGraph α) (M : Set (Sym2 α)) : Prop · SimpleGraph.IsEdgeDominating

IsEdgeMatching def

A finite set of edges M is a matching of G if every element of M is an edge of G and any two edges of M are equal or share no vertex (no vertex is covered twice). · SimpleGraph.IsEdgeMatching

IsEngelElement def

An element $y$ of a group $G$ is a (left) Engel element if for every $x \in G$ there is some $n$ with $[x,\, {}_n y] = 1$. · Kourovka.«1.40».IsEngelElement

IsEngelGroup def

A nilgroup (Engel group) is a group in which every element is an Engel element. · Kourovka.«1.40».IsEngelGroup

IsEpsilonLight def

For a graph $G = (V, E)$, let $G_S = (V, E(S,S))$ denote the graph with the same vertex set, but only the edges between vertices in $S$. Let $L$ be the Laplacian matrix of $G$ and let $L_S$ be the Laplacian of $G_S$. · Arxiv.«2602.05192».IsEpsilonLight

IsEquidistantOnCircle def

A is a set of equidistant points on a circle: there are a centre c, a radius r > 0, an initial angle θ and a non-zero angular step α such that A consists of the points of the circle of centre c and radius r at the angles `θ … · Erdos958.IsEquidistantOnCircle

IsEquidistantOnLine def

A is a set of equidistant points on a line: there are a point a and a non-zero direction v such that A consists of the points a + i • v for 0 ≤ i < #A. · Erdos958.IsEquidistantOnLine

IsEquidistributed def

A sequence (s_1, s_2, s_3, ...) of real numbers is said to be equidistributed on an interval [a, b] if for every subinterval [c, d] of [a, b] we have lim_{n→ ∞} |{s_1, ..., s_n} ∩ [c, d]| / n = (d - c)/(b-a) · IsEquidistributed

IsEquidistributedModuloOne def

A sequence (s_1, s_2, s_3, ...) of real numbers is said to be equidistributed modulo 1 or uniformly distributed modulo 1 if the sequence of the fractional parts of a_n, denoted by (a_n) or by a_n − ⌊a_n⌋, is equidistributed in the … · IsEquidistributedModuloOne

IsEquilateralTriangle def

A three-point set whose pairwise distances are all equal to side. · Erdos755.IsEquilateralTriangle

IsErdos944 def

The predicate that graph $G$ with chromatic number $k$ is such that every vertex is critical, yet every critical set of edges has size $>r$ · Erdos944.SimpleGraph.IsErdos944

IsErdosHajnalExceptional def

A pair $(G_1, G_2)$ is Erdős–Hajnal exceptional if it has both the finite Ramsey property and the countable Ramsey escape property. · SimpleGraph.IsErdosHajnalExceptional

IsErdosHajnalLowerBound def

For a graph $H$, consider all graphs $G$ that do not contain $H$ as an induced subgraph. We would like to find a lower bound $f(n)$ such that every such $G$ on $n$ vertices has a clique or independent set of size $\ge f(n)$ for … · Erdos61.IsErdosHajnalLowerBound

IsErdosLovaszFamily def

An Erdős–Lovász family of order n: an intersecting family of n-sets such that every set of size at most n - 1 is disjoint from some member. · Erdos21.IsErdosLovaszFamily

IsEssentialComponent def

We say that $A\subset \mathbb{N}$ is an essential component if $d_s(A \oplus B)>d_s(B)$ for every $B\subset \mathbb{N}$ with $0<d_s(B)<1$ where $d_s$ is the Schnirelmann density. Here, the sumset is the appropriate one for Schnirelmann … · Erdos1146.IsEssentialComponent

IsEulerBrick def

An Euler brick is a rectangular cuboid where all edges and face diagonals have integer lengths. · EulerBrick.IsEulerBrick

IsEulerHyperBrick def

Generalization of an Euler brick to $n$-dimensional space. · EulerBrick.IsEulerHyperBrick

IsExactAdditiveComplement def

Two sets $A, B\subseteq \mathbb{N}$ are exact additive complements if $A+B$ contains all large integers and $A(x)B(x)\sim x$. · Erdos785.IsExactAdditiveComplement

IsFactorial def

def IsFactorial (d : ℕ) : Prop · Erdos1059.IsFactorial

IsFactorialPrime def

A factorial prime is a prime one above or one below a factorial. · FactorialPrime.IsFactorialPrime

isFactorialPrime def

Factorial primes: $n$ such that $n! + 1$ is prime (A002981). · OeisA55487.isFactorialPrime

IsFarey def

A rational q is a Farey fraction of order n if it lies in [0, 1] and has denominator at most n. (Every q : ℚ is stored in lowest terms, so q.den and q.num are the reduced denominator and numerator.) · Erdos1005.IsFarey

IsFiniteUnionOfIntervals def

A set $A \subseteq \mathbb{R}$ is a finite union of intervals if it is a union of $n$ intervals for some $n$. · WeakTiling.IsFiniteUnionOfIntervals

IsFirstKindChainOfLength def

p starts a first-kind Cunningham chain of exact positive length k. · CunninghamChain.IsFirstKindChainOfLength

IsForbiddenTripleFree def

A finite set of naturals A is said to be forbidden-triple-free if for all a, b, c ∈ A, if a < min(b, c) then a does not divide b + c. · Erdos13.IsForbiddenTripleFree

IsFundamentalDiscr def

Fundamental discriminants are those integers D that appear as discriminants of quadratic fields. · NumberField.IsFundamentalDiscr

IsFusible inductive

A rational number is fusible if it belongs to the smallest set containing $0$ and closed under the operation $$ a \sim b = \frac{a + b + 1}{2} $$ whenever $|a-b| < 1$. · FusibleNumber.IsFusible

IsGauging def

g is a gauging for M with concentration c: it sums to 1 and M g is the constant vector c. This is Definition 2.3 of the source, which states it for symmetric M. · Arxiv.«2607.05349».IsGauging

IsGenericRank def

IsGenericRank ds r says that r is the generic rank of complex tensors of format ds: the tensors of rank r contain a dense open set. · Arxiv.«0805.3777».IsGenericRank

IsGenuinelySublacunary def

The sequence $m$ eventually grows at least geometrically with a logarithmic correction. · Bugeaud06.IsGenuinelySublacunary

IsGeodesic def

A word l is geodesic if its length is exactly the word length of the group element it represents. · Group.Generators.IsGeodesic

IsGood def

A sequence is "good" if 1. it is strictly monotone 2. it is pairwise coprime 3. the sum of reciprocals converges 4. the gap between consecutive elements in A(u) is bounded relative to t_x. · Erdos1101.IsGood

IsGood abbrev

A set A is "good" if it is infinite and there are no distinct a,b,c in A such that a ∣ (b+c) and b > a, c > a. · Erdos12.IsGood

IsGoodFor def

The predicate that A is monotone, A 0 = n and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j · Erdos359.IsGoodFor

IsGoodPair def

This defines the core property of the problem: For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete? · Erdos349.IsGoodPair

IsGoormaghtighNumber def

A number having repunit representations of at least three digits in two distinct bases. · Goormaghtigh.IsGoormaghtighNumber

IsGraphRamsey def

IsGraphRamsey n k l means that for every simple graph G on n vertices, either - G contains a clique of size k, or - the complement graph Gᶜ contains a clique of size l (equivalently, G contains an independent set of size … · RamseyNumbers.IsGraphRamsey

IsGreaterTwinPrime def

A prime $p$ is the greater of a twin prime pair if $p$ and $p - 2$ are both prime. · OeisA166944.IsGreaterTwinPrime

IsGroupSidon def

A subset $S$ of an abelian group is a Sidon set of the first kind in the sense of Babai and Sós [BS85] if $a + b = c + d$ with $a, b, c, d \in S$ implies $|\{a, b, c, d\}| \le 2$. · Green31.IsGroupSidon

IsHadamard def

A square matrix $M$ with $±1$-entries that satisfies the equality $|M| ≤ n^\frac{n}{2}$ is called a Hadamard matrix. · Hadamard.IsHadamard

IsHadamard' def

Equivalently, a square matrix $M$ with $±1$-entries $|A| ≤ n^\frac{n}{2}.$ if it satisfies the equality $M^TM = n \cdot 1$, where $1$ denotes the unit matrix. · Hadamard.IsHadamard'

IsHalting class

The property that a Turing Machine M eventually halts when starting from an empty tape · Turing.BusyBeaver.Machine.IsHalting

IsHaltingConfiguration def

M.HaltsAtConfiguration s is the predicate that M is a halting configuration for M. · Turing.BusyBeaver.Machine.IsHaltingConfiguration

IsHaltingInput def

M.IsHaltingInput l is the predicate that M is a halting configuration for M. · Turing.BusyBeaver.Machine.IsHaltingInput

IsHamiltonianCycle def

A Hamiltonian cycle of G: a cycle passing through every vertex. · LovaszPlummerConjecture.IsHamiltonianCycle

IsHofstadterQ def

IsHofstadterQ f means that $f$ is Hofstadter's $Q$-sequence (OEIS A005185): $f(1) = f(2) = 1$ and for $n > 2$ $$ f(n) = f(n - f(n - 1)) + f(n - f(n - 2)), $$ where the recurrence requires $f(n - 1) < n$ and $f(n - 2) < n$, so that both … · Erdos422.IsHofstadterQ

IsHofstadterSeq def

The Hofstadter sequence (OEIS A005243): $a(1) = 1$, $a(2) = 2$, and for $k \ge 3$, $a(k)$ is the least integer $> a(k-1)$ that equals the sum of at least two consecutive terms from $\{a(1), \ldots, a(k-1)\}$. The sequence begins $1, 2, 3, … · Erdos423.IsHofstadterSeq

IsHyperbolic class

A group G is hyperbolic if there exists a finite generating family P and a constant δ such that G is δ-hyperbolic with respect to P. · Group.IsHyperbolic

IsHyperbolic class

A pseudometric space is hyperbolic if it is δ-hyperbolic for some real constant δ. · Metric.IsHyperbolic

IsHyperbolicWith def

A group is δ-hyperbolic with respect to a generating family P if its induced metric space is δ-hyperbolic. · Group.Generators.IsHyperbolicWith

IsHyperbolicWith def

A pseudometric space is δ-hyperbolic if for all w x y z the four-point condition min (gromovProduct w x y) (gromovProduct w y z) - δ ≤ gromovProduct w x z holds. · Metric.IsHyperbolicWith

IsHypergraphIndependent def

No edge is contained in this set of vertices. · Finset.IsHypergraphIndependent

IsIdoneal def

Equivalent definition: A positive integer $n$ is idoneal if and only if it cannot be written as $ab + bc + ac$ for distinct positive integers $a, b,$ and $c$. · Idoneal.IsIdoneal

IsIncreasing₂ def

Since the $2$-less relation is not transitive, we make a further definition to specify transivity. · Arxiv.«1609.08688».IsIncreasing₂

IsIndepDominating def

def IsIndepDominating (G : SimpleGraph α) (D : Set α) : Prop · SimpleGraph.IsIndepDominating

IsIndependent def

X is independent for a set mapping f on pairs if f s(x, y) ∉ X whenever x ≠ y are in X. · Erdos1025.IsIndependent

isInducedC4 def

Check whether four distinct vertices form an induced 4-cycle in G. We test all three perfect-matching pairings of the four vertices to find a cyclic ordering and verify that the induced subgraph has exactly those 4 edges. · SimpleGraph.isInducedC4

isInducedPath def

Check if a list of vertices forms an induced path in G. · SimpleGraph.isInducedPath

IsIntegerValue def

$x_n$ takes an integer value. · Arxiv.«2607.05739».IsIntegerValue

IsIntegralDiophantineTuple abbrev

An integral Diophantine tuple is a Diophantine tuple of positive integers. · DiophantineTuple.IsIntegralDiophantineTuple

IsInterval def

A finite set of naturals is an interval of naturals. · Erdos363.IsInterval

IsIrrationalAlgebraic def

A real number is irrational algebraic if it is algebraic over ℚ but not rational. · AlgebraicNormality.IsIrrationalAlgebraic

IsIrrationalitySequence def

We call a strictly increasing sequence $a_n$ of positive integers an irrationality sequence if for any sequence $b_n$ of positive integers with $\frac{a_n}{b_n} \to 1$ as $n \to \infty$, the sum $\sum \frac{1}{b_n}$ converges to an … · Erdos263.IsIrrationalitySequence

IsIrrationalitySequence def

A sequence $a_n$ of integers is called an irrationality sequence if for every bounded sequence of integers $b_n$ with $a_n + b_n \neq 0$ and $b_n \neq 0$ for all $n$, the sum $$ \sum \frac{1}{a_n + b_n} $$ is irrational. · Erdos264.IsIrrationalitySequence

IsIsosceles def

def IsIsosceles {α : Type*} [Dist α] (p q r : α) : Prop · IsIsosceles

IsIsosceles def

def Set.IsIsosceles {α : Type} [Dist α] (A : Set α) · Set.IsIsosceles

IsIsoscelesFree def

A set is isosceles-free if no three distinct points in it form an isosceles triangle. · Set.IsIsoscelesFree

IsIsoscelesTrapezoid def

a b c d are the vertices, in counter-clockwise order, of an isosceles trapezoid: they are in strictly convex position, the side ab is parallel to the side cd (the two bases), and the diagonals ac and bd have equal length. One … · EuclideanGeometry.IsIsoscelesTrapezoid

IsJacobsthalBound def

IsJacobsthalBound k m says that every interval of m consecutive integers contains an integer coprime to every positive natural number having at most k distinct prime factors. · Erdos970.IsJacobsthalBound

IsKakeya def

A set S in ℝⁿ is called a Kakeya set if it contains a unit line segment in every direction. For simplicity, we omit the compactness assumption here. For a discussion on the equivalence of definitions with and without compactness, see … · Kakeya.IsKakeya

IsKakeyaFinite def

A finite field variant of the Kakeya problem considers subsets of 𝔽_qⁿ that contain a line in every direction. · Kakeya.IsKakeyaFinite

IsKChoosable def

A graph $G$ is $k$-choosable if for any assignment of a list of $k$ colours to each vertex of $G$ (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices … · Erdos753.IsKChoosable

IsKConnected def

G is k-connected: it has more than k vertices, and it stays connected after the removal of any set of fewer than k vertices. · SimpleGraph.IsKConnected

IsKFinite abbrev

f is K-finite: the span of its right K-translates is finite-dimensional. This is condition (b2) in the definition of an automorphic form. · AutomorphicForm.IsKFinite

IsLacunary def

Say a sequence is lacunary if there exists some $\lambda > 1$ such that $a_{n+1}/a_n > \lambda$ for all sufficiently large $n$. · IsLacunary

IsLacunaryReal def

The real-valued analogue of IsLacunary. · IsLacunaryReal

IsLargestNegFundDiscrForClassNumber def

$|d|$ is the largest absolute value among negative fundamental discriminants with class number $n$. · OeisA38552.IsLargestNegFundDiscrForClassNumber

IsLcmFree def

A set A ⊆ {1, …, n} such that lcm(a, b) > n for all distinct a, b ∈ A. · Erdos542.IsLcmFree

IsLeinster def

A finite group G is a Leinster group if the sum of the orders of all its normal subgroups equals twice the group's order. · LeinsterGroup.IsLeinster

IsLexIdeal def

A lex ideal is a monomial ideal L such that for monomials u, v of the same degree with u larger than v in the lexicographic order, v ∈ L implies u ∈ L. Here the variables are ordered by $x_1 > x_2 > \dots > x_n$, which for … · MvPolynomial.IsLexIdeal

IsLine def

A line in the plane: an affine subspace of ℝ² whose direction is one-dimensional. · EuclideanGeometry.IsLine

IsLinearHypergraph def

Distinct edges intersect in at most one vertex. · Finset.IsLinearHypergraph

IsLineCover def

S is a set of points of $\{1,\ldots,n\}^2$ such that the lines determined by the pairs of distinct points of S cover all points of $\{1,\ldots,n\}^2$. · Erdos798.IsLineCover

IsLocallyRightLinear def

An order automorphism $f$ of $\mathbb{R}$ is locally right $H$-linear if every point has a right neighbourhood on which $f$ is affine with slope in $H \le \mathbb{R}_{>0}$. · Kourovka.«21.149».IsLocallyRightLinear

IsLPF def

IsLPF p m says that p is the least prime factor of m. · Erdos681.IsLPF

IsLucasSequence def

We define a Lucas sequence to be a Fibonacci sequence with arbitrary starting points L 0 and L 1. · Erdos276.IsLucasSequence

IsLucasWieferichPrime structure

Lucas–Wieferich prime A Lucas–Wieferich prime associated with $(a,b)$ is an odd prime $p$, not dividing $a^2 - 4b$, such that $U_{p-\varepsilon}(a,b) \equiv 0 \pmod{p^2}$ where $U(a,b)$ is the Lucas sequence of the first kind and … · IsLucasWieferichPrime

IsLychrel10 def

The number $n$ is a (base-10) Lychrel number if no iterate of the Lychrel process is a palindrome. · LychrelNumbers.IsLychrel10

IsMaximal class

A right ideal is maximal if it is maximal among the proper right ideals. · RightIdeal.IsMaximal

IsMaximal def

A complete ruler is maximal if no complete ruler with the same number of marks (equivalently, the same number of segments) has greater length. · SparseRuler.IsMaximal

IsMaximalAddFactorsCard def

def IsMaximalAddFactorsCard (f : ℕ → ℕ) : Prop · Erdos126.IsMaximalAddFactorsCard

IsMaximalEdgeMatching def

A matching M of G is maximal if no further edge of G can be added to M while keeping the matching property. · SimpleGraph.IsMaximalEdgeMatching

IsMaximalRun def

def IsMaximalRun (v : ℕ) (n L : ℕ) : Prop · OeisA271591.IsMaximalRun

IsMaximalSidonSetIn def

IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and cannot be extended within {1, …, N} while remaining Sidon. · Set.IsMaximalSidonSetIn

IsMaximalSumFree def

A is a maximal sum-free subset of {1, …, n}. · Erdos877.IsMaximalSumFree

IsMaxMUBCount def

$k$ is the maximal size of a family of mutually unbiased bases in dimension $d$. · OpenQuantumProblem13.IsMaxMUBCount

IsMaxNoTripleCard def

$f N$ is the size of the largest $A ⊆ \{1, …, N\}$ containing no solution to $\frac{1}{a} = \frac{1}{b} + \frac{1}{c}$ with distinct $a, b, c ∈ A$. · Erdos302.IsMaxNoTripleCard

IsMaxRank def

IsMaxRank ds r says that r is the maximal rank of a complex tensor of format ds: every such tensor has rank at most r, and some tensor has rank r. · Arxiv.«0805.3777».IsMaxRank

IsMills abbrev

Given any real $A$, IsMills A encodes the statement that $\lfloor A^{3^n}\rfloor,n > 0$ is prime. · Mills.IsMills

IsMinimal def

A complete ruler is minimal if no complete ruler of the same length $L$ has fewer marks (equivalently, fewer segments). · SparseRuler.IsMinimal

IsMinimalAsymptoticAddBasisOfOrder def

We interpret "additive basis of order k" as an asymptotic additive basis of order k, using the predicate Set.IsAsymptoticAddBasisOfOrder from additive combinatorics. · Erdos881.IsMinimalAsymptoticAddBasisOfOrder

IsMinimalCut def

A minimal cut of a graph G is a minimal set T of vertices whose removal disconnects G, that is, G - T fails to be preconnected while G - S is preconnected for every S ⊂ T. · Erdos150.IsMinimalCut

IsMinimalDistinctCoveringSystem def

A minimal distinct covering system: valid classes with distinct moduli that cover ℤ, with no proper subset already covering. · Erdos1188.IsMinimalDistinctCoveringSystem

IsMinimalTopologicalGroup def

A minimal topological group in Platonov's sense: a non-discrete Hausdorff topological group all of whose proper closed subgroups are discrete. · Kourovka.«1.74».IsMinimalTopologicalGroup

IsMinimalTotalDominatingSet def

A total dominating set S is minimal if no proper subset of S is also a total dominating set. · SimpleGraph.IsMinimalTotalDominatingSet

IsMinimiser def

A is a minimiser for n if it is a separated set of n points whose diameter is at most the diameter of every separated set of n points (compare Erdos99.erdos_99). · Erdos103.IsMinimiser

IsMinMills abbrev

For a real $A$, IsMinMills A is the smallest value satisfying IsMills A. · Mills.IsMinMills

IsMirimanoffPrime abbrev

Mirimanoff prime A Mirimanoff prime is a prime $p$ with $3^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $3$. The name comes from Mirimanoff's 1910 result that a failure of the first case of Fermat's Last Theorem for the … · IsMirimanoffPrime

IsMonochromatic def

A set A ⊆ α is monochromatic under a 2-colouring f : α → Fin 2 if all elements of A receive the same colour. · Erdos602.IsMonochromatic

IsMonochromaticBox def

A subset $A_1 \times B_1 \times C_1$ of $A \times B \times C$ is monochromatic under a 2-colouring $f : A \to B \to C \to \operatorname{Fin} 2$ if $f$ is constant on $A_1 \times B_1 \times C_1$. · Erdos1128.IsMonochromaticBox

IsMonomialIdeal def

An ideal of a polynomial ring is a monomial ideal if it is generated by monomials. · MvPolynomial.IsMonomialIdeal

IsMonotoneIncreasing abbrev

A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$ contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes" and "up-families".) From now on we will restrict … · Mathoverflow10799.IsMonotoneIncreasing

IsMostFrequent def

$v_0$ is a most frequent value among $a(1), \dots, a(x)$. · OeisA182126.IsMostFrequent

IsMovingSofa structure

A connected closed set $s$ is a moving sofa according to a rigid motion $m:I\to\mathrm{SE}(2)$, if the sofa is initially in the horizontal side of the hallway and ends up in the vertical side. Here, since $\mathrm{SE}(2)$ is not in … · MovingSofa.IsMovingSofa

IsMUBFamily def

A family of unitary matrices is a family of mutually unbiased bases if every two distinct members are unbiased. · OpenQuantumProblem13.IsMUBFamily

IsMulBasis def

An additive basis of some order. · Set.IsMulBasis

IsMulBasisOfOrder def

def IsMulBasisOfOrder (A : Set M) (n : ℕ) : Prop · Set.IsMulBasisOfOrder

IsMulCardSet def

Nat.IsMulCardSet A means that A is a set of natural numbers that satisfies the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$. · Erdos786.Set.IsMulCardSet

IsNColorable def

A weak proper coloring using at most n colors. · Hypergraph.IsNColorable

IsNColorable abbrev

A weak proper coloring using at most n colors. · UniformHypergraph.IsNColorable

IsNDominatingSet structure

An n-dominating set is a dominating set with n vertices. · SimpleGraph.IsNDominatingSet

IsNearTransversal abbrev

A near-transversal of a latin square L of order n is a selection of n - 1 cells, given by a row-selector ρ and a column-selector σ (both Fin (n - 1) → Fin n), such that the selected rows are all distinct, the selected columns … · IsNearTransversal

IsNEdgeDominatingSet structure

structure IsNEdgeDominatingSet (n : ℕ) (M : Finset (Sym2 α)) : Prop · SimpleGraph.IsNEdgeDominatingSet

IsNetwork def

A family N of subsets of a topological space X is a network for X if every open subset of X is a union of members of N. Unlike the members of a topological basis, the members of a network need not be open. · TopologicalSpace.IsNetwork

IsNil def

Say a subset I of a ring R is nilpotent if all its elements are nilpotent. · Koethe.IsNil

IsNIndepDominatingSet structure

structure IsNIndepDominatingSet (n : ℕ) (D : Finset α) : Prop · SimpleGraph.IsNIndepDominatingSet

IsNontrivial def

A pair $(q, a)$ describes a non-trivial arithmetic progression if $q, a \ge 1$, $\gcd(q, a) = 1$, and $(q, a) \neq (1, 1)$. · RudinsConjecture.IsNontrivial

IsNormalInBase def

A real number x is normal in base b if every string w of k digits < b appears with asymptotic frequency 1 / b ^ k in the base-b fractional expansion of x, that is, the proportion of positions i < n at which w occurs … · NormalNumber.IsNormalInBase

IsNormalisedEigenform def

Since we don't have Hecke operators yet, we define this via the q-expansion coefficients. See Proposition 5.8.5 of [diamondshurman2005]. · ModularityConjecture.IsNormalisedEigenform

IsNormalized structure

Goodman's normalisation $f(z) = \sum_{n \ge 1} b_n z^n$, i.e. $f(0) = 0$. · GoodmanConjecture.IsNormalized

IsNormalized def

A state vector is normalized if it has $L^2$ norm $1$. · OpenQuantumProblem23.IsNormalized

IsNormalized def

A state vector is normalized if it has $L^2$ norm $1$. · OpenQuantumProblem35.IsNormalized

IsObligatory def

A finite uniform hypergraph is obligatory if it appears in every hypergraph of that uniformity whose chromatic cardinal exceeds ℵ₀. · UniformHypergraph.IsObligatory

IsOeisPrimePower def

A number $n$ is an "OEIS prime power" (for the context of A113609's definition) if $n=1$ or $n$ is a standard prime power. · OeisA113609.IsOeisPrimePower

IsOfClass def

A prime $p$ is in class $1$ if the only prime divisors of $p+1$ are $2$ or $3$. In general, a prime $p$ is in class $r$ if every prime factor of $p+1$ is in some class $\leq r-1$, with equality for at least one prime factor. · Erdos1055.IsOfClass

IsOnePeriodic def

A function $f : \mathbb{R}^n \to \alpha$ is 1-periodic if it is periodic in each coordinate with period $1$, i.e. $f(x + e_i) = f(x)$ for each unit vector $e_i$. This captures functions on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$. · NavierStokes.IsOnePeriodic

IsOptimal def

A set $A$ is 'optimal' if it has $n$ points and achieves the minimum distance count. · Erdos91.IsOptimal

IsOptimal def

We say that a family is optimal for $\mu_p$ if the isoperimetric inequality (IR) is sharp up to a multiplicative constant $1000 \log (1/p)$. · Mathoverflow10799.IsOptimal

IsOptimal def

A ruler is optimal if it is both minimal and maximal. · SparseRuler.IsOptimal

IsOptimalWith def

Following Kahn–Kalai, a family is $(C \log(1/p), p)$-optimal if the isoperimetric inequality (IR) is sharp up to the multiplicative constant $C \log(1/p)$, i.e. $$I^p(\mathcal F) \le \frac{C}{p} \cdot \mu_p(\mathcal F) \cdot \log … · Mathoverflow10799.IsOptimalWith

IsOrientation def

An orientation of an undirected simple graph H is a digraph D whose edges are obtained by directing each edge of H in exactly one direction. · Digraph.IsOrientation

IsPacking def

A "packing" means that the interiors of any two rectangles are disjoint. · Mathoverflow34145.Configuration.IsPacking

IsPairwiseBalancedDesign def

A pairwise balanced design, permitting a block equal to the ground set. · Finset.IsPairwiseBalancedDesign

IsPalindrome10 def

A number is a (base-10) palindrome if it equals its digit reversal. · LychrelNumbers.IsPalindrome10

IsParallelogramAtOrigin def

$K$ is a parallelogram with a vertex at the origin: the convex hull of $0$, $a$, $b$ and $a + b$ for linearly independent $a$, $b$. · Arxiv.«2607.03582».IsParallelogramAtOrigin

IsPathCover def

A family of paths covering all vertices without overlaps. · SimpleGraph.IsPathCover

IsPathSubgraph def

A subgraph H of G is a path subgraph if it is the subgraph traced out by a path in G, i.e. a walk with no repeated vertices. · Erdos583.IsPathSubgraph

IsPebblingMove def

A pebbling move on a graph consists of choosing a vertex with at least two pebbles, removing two pebbles from it, and adding one to an adjacent vertex (the second removed pebble is discarded from play). · PebblingNumberConjecture.IsPebblingMove

IsPerfectCuboid def

A perfect cuboid is an Euler brick with an integer space diagonal. · EulerBrick.IsPerfectCuboid

IsPerfectDifferenceSet def

A perfect difference set modulo n is a set D such that the map (a, b) ↦ a - b from D.offDiag to {x : ZMod n | x ≠ 0} is a bijection. · IsPerfectDifferenceSet

IsPerfectPower def

A perfect power is a natural number that is a product of equal natural factors, or, in other words, an integer that can be expressed as a square or a higher integer power of another integer … · Nat.IsPerfectPower

IsPiecewiseMvPolynomial def

A function f : ℝⁿ → ℝ is piecewise polynomial if there exists a finite covering of ℝⁿ by closed semi-algebraic sets such that the restriction of f to each set in the covering is polynomial. · PierceBirkhoff.IsPiecewiseMvPolynomial

IsPiecewisePolynomial def

A function f : ℝ → ℝ is piecewise polynomial if there exists a finite covering of ℝ by closed semi-algebraic sets such that the restriction of f to each set in the covering is polynomial. · PierceBirkhoff.IsPiecewisePolynomial

IsPierpontPrime def

A Pierpont prime is a prime of the form $2^a3^b + 1$. · PierpontPrime.IsPierpontPrime

IsPisot def

A Pisot–Vijayaraghavan number is a real algebraic integer θ > 1 all of whose other conjugates lie strictly inside the complex unit disc: every root in ℂ of the minimal polynomial of θ over ℚ, except θ itself, has modulus `< … · IsPisot

IsPoissonEndomorphism def

A K-algebra endomorphism φ of the polynomial algebra in $2n$ variables is an endomorphism of the n-th canonical Poisson algebra $P_n(K)$ if it preserves the canonical Poisson bracket. Following [AvdE07], Lemma 2, it is equivalent to … · Arxiv.«math.0608009».IsPoissonEndomorphism

IsPolyhedronVertices def

P is the set of vertices of a (full-dimensional) convex polyhedron in $\mathbb{R}^3$: the points are in convex position and they affinely span $\mathbb{R}^3$ (so the polyhedron is genuinely three-dimensional). · Erdos660.IsPolyhedronVertices

IsPolyTime def

A function is polynomial-time computable when it is IsPolyTimeWithEncoding for the canonical Bool-alphabet encodings of its domain and codomain as given by the BitstringEncoding typeclass. · ComplexityTheory.IsPolyTime

IsPolyTimeWithEncoding def

IsPolyTimeWithEncoding ea eb f asserts that f is computable in polynomial time when its input and output are encoded via the given Encodings ea and eb. · ComplexityTheory.IsPolyTimeWithEncoding

isPositiveList def

A list of natural numbers is composed of positive integers. · OeisA52709.isPositiveList

IsPositiveUnitWalk def

A sequence $a_1, a_2, \ldots \in \mathbb{R}^d$ such that every difference $a_{i+1}-a_i$ is a positive unit vector $(0,\ldots,0,1,0,\ldots,0)$. · Erdos192.IsPositiveUnitWalk

IsPower def

$n$ is a perfect power if there exist natural numbers $m$ and $l$ such that $1 < l$ and $m^l = n$. · Erdos930.IsPower

IsPractical def

A natural number $n$ is practical if every positive integer $m ≤ n$ can be represented as a sum of distinct divisors of $n$. · Nat.IsPractical

IsPrimaryPseudoperfect def

An integer n is a primary pseudoperfect number if it is the denominator m in a solution (m, P) to the Erdős 313 problem. · Erdos313.IsPrimaryPseudoperfect

isPrimeBitsSet def

Primes with $m$ one bits in their binary representation. · OeisA81091.isPrimeBitsSet

IsPrimeConstellation def

A prime constellation is a tuple $(p, p + m_1, \dots, p + m_k)$ such that the $m_i$ are all positive even integers and every entry is a prime number. · HardyLittlewood.IsPrimeConstellation

IsPrimeProgressionOfLength def

The predicate that a set s consists of l consecutive primes (possibly infinite). This predicate does not assert a specific value for the first term. · Erdos141.Set.IsPrimeProgressionOfLength

IsPrimitive def

A set is primitive if no non-associated elements of the set divide each other. · Erdos1196.IsPrimitive

IsPrimitive def

A primitive subset of $\{2, \dots, n\}$ is a set in which no element divides another. The quantified divisibility condition is one-sided because the variables range over all ordered pairs of distinct elements. · Erdos872.IsPrimitive

IsPrimitive def

An element n is primitive in a set S ⊆ ℕ if n ∈ S and no proper divisor of n is in S. · Set.IsPrimitive

IsPrimitiveTerm abbrev

A term $n$ is primitive if no proper divisor of $n$ is in the sequence. · OeisA63880.IsPrimitiveTerm

IsProductFree def

def IsProductFree {M : Type*} [Mul M] (S : Set M) : Prop · IsProductFree

IsProperColoring def

A weak proper coloring gives two vertices different colors in every edge. · Hypergraph.IsProperColoring

IsProperColoring abbrev

Weak proper coloring of the underlying Mathlib hypergraph. · UniformHypergraph.IsProperColoring

IsProperHypergraphColoring def

A weak proper coloring has no monochromatic edge. · Finset.IsProperHypergraphColoring

IsProperTiling def

A proper tiling of $\Omega^c$ by translates of $\Omega$ is specified by a set of translation parameters $T \subseteq \mathbb{R}$ such that the sum of Dirac masses on $T$ is a weak tiling measure for $\Omega$. · WeakTiling.IsProperTiling

IsProportionatelyDissociated def

We call $A$ proportionately dissociated if every finite $B\subset A$ contains a dissociated set of size $\gg \lvert B\rvert$. · Set.IsProportionatelyDissociated

isProved def

Whether declName has a proof term with no sorry in it, waiting on the declaration to finish elaborating. · FormalProofLinter.isProved

IsPseudoSelfridge structure

A number p satisfies the Pseudo Selfridge condition if 1. p is odd, 2. p ≡ ± 1 (mod 5), 3. 2^(p-1) ≡ 1 (mod p) 4. (p-1).fib ≡ 0 (mod p) · Selfridge.IsPseudoSelfridge

IsPurelySingularOn def

A function $f : \mathbb{R} \to \mathbb{R}$ is purely singular (or singular continuous) on a set $s \subseteq \mathbb{R}$ if it is continuous on $s$ and its derivative within $s$ equals zero almost everywhere on $s$ with respect to Lebesgue … · Erdos50.IsPurelySingularOn

IsPValent structure

A function f : ℂ → ℂ is $p$-valent on the open unit disk $\mathbb{D} = \{z : |z| < 1\}$ if it is analytic there, attains every value at most $p$ times, and attains some value exactly $p$ times. Here $p \ge 1$. Values are counted at … · GoodmanConjecture.IsPValent

IsQuasiLineGraph def

A graph is a quasi-line graph if the neighborhood of every vertex can be partitioned into two cliques. · SimpleGraph.IsQuasiLineGraph

IsRademacherMultiplicative structure

A random function $f$ is Rademacher multiplicative if $f(1) = 1$, for each prime $p$, we independently choose $f(p) \in \{-1, 1\}$ uniformly at random (so each $f(p)$ is a measurable function of the sample point), for each square-free … · Erdos520.IsRademacherMultiplicative

IsRainbow def

A homomorphism f : H →g G is rainbow for an edge labeling c of G if it maps distinct edges of H to edges of G with distinct labels. · SimpleGraph.IsRainbow

IsRamseySizeLinear def

A graph G is Ramsey size linear if there exists a constant c > 0 such that for all graphs H with m edges and no isolated vertices, the Ramsey number satisfies R(G, H) ≤ c · m. · SimpleGraph.IsRamseySizeLinear

IsRatioBasis def

def IsRatioBasis (A S : Finset G) : Prop · Finset.IsRatioBasis

IsRationalDiophantineTuple abbrev

A rational Diophantine tuple is a Diophantine tuple of nonzero rationals. · DiophantineTuple.IsRationalDiophantineTuple

IsRationalExtension class

A rational field extension is a field extension L/K isomorphic to a field of rational functions (in some arbitrary number of indeterminates.) · NoetherProblem.IsRationalExtension

IsReachable def

A pebble distribution B is reachable from another pebble distribution A, if there exists a sequence of pebbling moves transforming the first into the second. · PebblingNumberConjecture.IsReachable

IsRealizable class

Say a group G is realizable over a field K if it is isomorphic to the Galois group of a Galois extension of K · InverseGalois.IsRealizable

IsRectangle structure

Four points a b c d in the plane form a rectangle with a opposite to c iff the line segments from a to c and from b to d have both the same length and the same midpoint, acting as the diagonals of the rectangle. We also … · InscribedSquare.IsRectangle

IsRecursive def

A set of sentences T is recursive if there is a computable function f : ℕ → Bool such that, for every sentence φ, f returns true on the Gödel number of φ if and only if φ ∈ T. · FirstOrder.Language.Theory.IsRecursive

IsRecursivelyBuiltMr def

G belongs to the class $M_r$, meaning it is built from $K_2$ by $r - 2$ generalised Mycielskians. Stiebitz's theorem is about this class and not about arbitrary graphs: it is false that $\chi(M_s(H)) = \chi(H) + 1$ for every $H$ and … · Erdos750.IsRecursivelyBuiltMr

IsRegularInduced def

A predicate that holds if $S$ is a regular induced subgraph of $G$ · Erdos82.IsRegularInduced

IsRegularPrime def

A natural prime number p is regular if p is coprime with the order of the class group of the p-th cyclotomic field. · RegularPrimes.IsRegularPrime

IsRepresentable def

IsRepresentable f n states that n can be written as 2 ^ k + m for some k ≥ 0 where the number of prime divisors of m, counted with multiplicity, is less than f m. · Erdos205.IsRepresentable

IsRepresentable def

k is representable as a sum of distinct unit fractions with denominators from {1, …, N}. · Erdos308.IsRepresentable

IsRepresentableAs abbrev

A natural $n$ is representable as a set $A$ if it can be written as the sum of finitely many elements of $A$ (with repetition allowed). · Erdos434.Nat.IsRepresentableAs

IsRightAngled def

a b c are the vertices of a right-angled triangle: the (unoriented) angle at one of the three vertices equals π / 2. · EuclideanGeometry.IsRightAngled

IsRightNoetherianRing abbrev

A semiring is right Noetherian if it is Noetherian as a right module over itself. · IsRightNoetherianRing

IsRupert def

A convex polyhedron (given as a finite collection of vertices) is Rupert if there are two rotations in ℝ³ (called "inner" and "outer") and a translation in ℝ² such that the "inner shadow" (the projection to ℝ² of the inner rotation applied … · Rupert.IsRupert

IsSecondKindChainOfLength def

p starts a second-kind Cunningham chain of exact positive length k. · CunninghamChain.IsSecondKindChainOfLength

IsSelfridge structure

A number p satisfies the Selfridge condition if 1. p is odd, 2. p ≡ ± 2 (mod 5), 3. 2^(p-1) ≡ 1 (mod p) 4. (p+1).fib ≡ 0 (mod p) · Selfridge.IsSelfridge

IsSemiAlgebraic def

A set is semi-algebraic in ℝⁿ if it can be described by a finite union of sets, each defined by finitely many simultaneous multivariate polynomial equations and strict inequalities. · PierceBirkhoff.IsSemiAlgebraic

IsSemiAlgebraic₁ def

A set is semi-algebraic in ℝ if it can be described by a finite boolean combination of polynomial equations and inequalities. · PierceBirkhoff.IsSemiAlgebraic₁

IsSendov def

The predicate that a polynomial satisfies the hypotheses of Sendov's conjecture. · Sendov.Polynomial.IsSendov

IsSeparated' def

A set s is ≥ ε-separated if its elements are pairwise at distance greater or equal to ε from each other. · Metric.IsSeparated'

IsShared def

A vertex is shared if it lies in two different cliques. · Erdos19.EFLConfig.IsShared

IsShiftEquivariant def

A map τ : (G → A) → (G → A) is equivariant (with respect to the left shift action) if τ(shift g x) = shift g (τ x) for all g : G and x : G → A. · GottschalkSurjunctivity.IsShiftEquivariant

IsSICFamily def

A SIC family in dimension $d$ consists of $d^2$ normalized vectors in $\mathbb{C}^d$ with pairwise squared overlap $(d + 1)^{-1}$. · OpenQuantumProblem23.IsSICFamily

IsSidon def

A Sidon set is a set, such that such that all pairwise sums of elements are distinct apart from coincidences forced by the commutativity of addition. · IsSidon

IsSierpinskiNumber def

A positive odd integer $k$ is a Sierpiński number if $k \cdot 2^n + 1$ is composite for all natural numbers $n$. In other words, every member of the set ${k \cdot 2^n + 1 : n \in … · Nat.IsSierpinskiNumber

IsSimiliCuttable def

A triangle is n-simili-cuttable if it can be decomposed into n similar triangles. · Erdos633.IsSimiliCuttable

IsSimplyNormalInBase def

A real number x is simply normal in base b if every digit d < b appears with asymptotic frequency 1 / b in the base-b fractional expansion of x. · NormalNumber.IsSimplyNormalInBase

IsSlowlyIncreasing def

A function φ : GL n ℝ → ℂ is slowly increasing, or of moderate growth, if ‖φ y‖ ≤ C * ‖y‖ ^ r for some real C and natural number r. This is condition (d) in the definition of an automorphic form. · Matrix.GeneralLinearGroup.IsSlowlyIncreasing

IsSmallCohenMacaulay structure

A small Cohen-Macaulay module over a local ring R is a finitely generated R-module M, necessarily nonzero, such that some system of parameters of R is a regular sequence on M. Such a module is also called a maximal … · Module.IsSmallCohenMacaulay

IsSmoothAdelic structure

Smoothness of a function on G(𝔸) = G(𝔸_f) × G(ℝ), with G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ]: continuous, locally constant in the finite variable, and C^∞ in the archimedean variable. · Matrix.GeneralLinearGroup.IsSmoothAdelic

IsSmoothOnGL def

φ : GL n ℝ → ℂ is C^∞: it extends to a C^∞ function on the open set of invertible matrices. Stating it this way avoids putting a manifold structure on GL n ℝ. · Matrix.GeneralLinearGroup.IsSmoothOnGL

IsSnakeInGraphOfLength def

A subgraph G' is a 'snake' of length k in graph G if it is an induced path of length k. · SnakeInBox.IsSnakeInGraphOfLength

IsSnug def

Characterizes a "snug" finite set of natural numbers: all elements are within a multiplicative factor $(1 + ε)$ of the minimum. Specifically, for a finite set $A$ and $ε > 0$, all $a ∈ A$ satisfy $a < (1 + ε) · min(A)$. · Erdos123.IsSnug

IsSolitary def

A positive integer $n$ is solitary if every friend of $n$ is equal to $n$, i.e. its abundancy class is the singleton $\{n\}$. · SolitaryNumber.IsSolitary

IsSolution def

n is a solution if n ∈ [p_{k-1}, p_k) for some k (with the convention p_0 = 1, where p_1 = 2 < p_2 < ⋯ are the primes) and the only primes dividing n! + 1 are p_k and p_{k+1}. Primes are indexed from 0 by `Nat.nth … · Erdos1058.IsSolution

IsSolutionOfAlgebraicODE def

A power series $f$ is a solution of an algebraic ODE defined by the rational function $g \in \mathbb{Q}(z, y_0, \dots, y_{n-1})$ if $f^{(n)}(z) = g(z, f(z), f'(z), \dots, f^{(n-1)}(z))$ and $g(0, f(0), f'(0), \dots, f^{(n-1)}(0))$ is … · LamLitt.IsSolutionOfAlgebraicODE

IsSpecialForm def

Holds when there is exists a number k such that $p = 2^k \\pm 1$ or $p = 4^k \\pm 3$. · Mersenne.Nat.IsSpecialForm

isSpectral def

A set is spectral if it belongs to a spectral pair. · isSpectral

IsSperner def

A Sperner family (antichain) of subsets of Fin n: a family of sets such that no member is a subset of another. · DedekindNumber.IsSperner

IsSpider234 def

The $(2,3,4)$-spider tree. A tree composed of three paths of lengths 2, 3, and 4 joined at a single central vertex: the centre is the unique vertex of degree 3 (every other vertex has degree at most 2), so the tree has exactly three … · SidorenkoConjecture.IsSpider234

IsSplitGraph def

A graph is a split graph if its vertex set splits into a clique and an independent set. · SimpleGraph.IsSplitGraph

IsStrongGiuga def

A (strong) Giuga number is a composite number $n$ such that $$\sum_{i=1}^{n - 1}i^{n - 1} \equiv -1\pmod{n}$$ · AgohGiuga.IsStrongGiuga

IsStronglyComplete def

The predicate that a set A is strongly complete, i.e. that for every finite set B, every sufficiently large integer is a sum of elements of the set A \ B. · Erdos351.IsStronglyComplete

IsSublacunary def

def IsSublacunary (m : ℕ → ℕ) : Prop · IsSublacunary

IsSubsetSumSeparatingCard def

Given a non-negative integer $n$, we say $m$ is a separating cardinality of subset sums if, for any set $A$ of $n$ integers, there is some $B\subseteq A$ of size $\geq m$ such that subset sums of $B$ can only ever coincide when the subsets … · Erdos789.IsSubsetSumSeparatingCard

IsSufficientScale def

Y ε n is a sufficient window length: for every ε > 0, all large n, and every y ≥ Y ε n, the window is ε-sparse. · Erdos450.IsSufficientScale

IsSuffixPrefixAvoiding def

Two sets of words $A, B$ over Fin q of length n are suffix-prefix avoiding if no nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. · SuffixPrefixAvoidance.IsSuffixPrefixAvoiding

IsSumDistinctRealSet abbrev

A finite set of real numbers is said to be sum-distinct if all the subset sums differ by at least $1$. · Erdos1.IsSumDistinctRealSet

IsSumDistinctSet abbrev

A finite set of naturals $A$ is said to be a sum-distinct set for $N \in \mathbb{N}$ if $A\subseteq\{1, ..., N\}$ and the sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ · Erdos1.IsSumDistinctSet

IsSumDivisors def

The proposition that n is a sum of distinct proper divisors. · Erdos469.Nat.IsSumDivisors

IsSumOfDistinct def

An integer n can be written as a sum of distinct elements of A. · Erdos254.IsSumOfDistinct

IsSumOfThreeCubes def

The predicate that n : R is a sum of three cubes. · SumOfThreeCubes.IsSumOfThreeCubes

IsSumOfTwoSquares def

A natural number is a sum of two squares if it can be written as a ^ 2 + b ^ 2. · Green66.IsSumOfTwoSquares

IsSumSqOfLength def

IsSumSqOfLength n a means that a is a sum of n squares. · IsSumSqOfLength

IsSumThreePower def

A predicate for $n$ to be the sum of three $k$th powers. · Erdos325.IsSumThreePower

IsSunflower def

A sunflower F is a collection of sets in which all possible distinct pairs of sets share the same intersection. · IsSunflower

IsSunflowerWithKernel def

A sunflower F with kernel S is a collection of sets in which all possible distinct pairs of sets share the same intersection S. · IsSunflowerWithKernel

IsSurjunctive def

A group G is surjunctive if for every finite nonempty type A, every injective, continuous, shift-equivariant map (G → A) → (G → A) is also surjective. · GottschalkSurjunctivity.IsSurjunctive

IsSWalk def

An $S$-walk is a sequence where every difference is in $S$. · Erdos193.IsSWalk

IsSynchronizing def

A DFA M is synchronizing if it has at least one synchronizing word. · DFA.IsSynchronizing

IsSynchronizingWord def

A word w is a synchronizing word (or reset word) for a DFA M if reading w from any state leads to the same single state. · DFA.IsSynchronizingWord

IsSyndetic def

A set $A$ of natural numbers is said to have bounded gaps if there exists an integer $p$ such that $A ∩ [n, n + 1, ..., n + p]$ is nonempty for all $n$. · IsSyndetic

IsSystemOfParameters structure

A system of parameters of a local ring R is a list of ringKrullDim R elements of R generating an ideal whose radical is the maximal ideal. · IsLocalRing.IsSystemOfParameters

IsTarskiMonster def

A Tarski monster group: an infinite group in which every non-trivial proper subgroup has order a fixed prime $p$. · Kourovka.«1.74».IsTarskiMonster

IsTaxicabFor def

$x$ is a taxicab number if it is the smallest number that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways. · Taxicab.IsTaxicabFor

IsTaxicabFor' def

$x$ is a candidate for being a taxicab number for $k, m, n$ if there exist at least $n$ distinct multisets of $m$ positive integers such that the sum of the $k$-th powers of the elements of each multiset is $x$. Using multisets means that … · Taxicab.IsTaxicabFor'

IsTestFunction def

The additive condition on test functions. The property in [Co26] that $\hat{g}(\pm i/2) = 0$, where $\hat{g}$ is the Mellin transform, corresponds to the vanishing of the Fourier transform at $\pm 1/2$. · RiemannHypothesis.IsTestFunction

IsThick def

A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$ · Erdos26.IsThick

IsTiling def

tiles is an exact decomposition of the unit n-cube into k homothetic cubes: every tile is a positive homothet inside the unit cube, and every point of [0,1)^n belongs to exactly one half-open tile. · Erdos769.IsTiling

IsTnInvariant def

A set $F$ is $T_n$-invariant if $T_n(F) \subseteq F$. · Arxiv.id2303_01089.IsTnInvariant

IsTorsionFree def

A predicate on an additive monoid saying that only 0 has finite order. · Monoid.IsTorsionFree

IsTotalDominating def

A set D is a total dominating set if every vertex is adjacent to a vertex in D. · SimpleGraph.IsTotalDominating

IsTotalDominatingSet def

A set S is a total dominating set of G if every vertex has a neighbor in S. · SimpleGraph.IsTotalDominatingSet

IsTotalNDominatingSet structure

An n-total dominating set is a total dominating set with n vertices. · SimpleGraph.IsTotalNDominatingSet

IsTournament def

A tournament is a directed graph in which every pair of distinct vertices is connected by exactly one directed edge. · Digraph.IsTournament

IsTransversal abbrev

A transversal of a latin square L is a selection of one cell per row, given by a column-selector σ, such that the selected columns are all distinct and the symbols at the selected cells are all distinct. · IsTransversal

IsTrianglesPlusHamiltonianCycle def

G is a graph on 3n vertices formed by taking n vertex-disjoint triangles T and adding a Hamiltonian cycle C (with all new edges): G = T ⊔ C with T and C edge-disjoint. · Erdos842.IsTrianglesPlusHamiltonianCycle

IsTriangular def

A natural number $n$ is triangular if $n = k(k+1)/2$ for some $k \in \mathbb{N}$. · OeisA185895.IsTriangular

IsTrivialSet def

A set s of vertices of a graph G is trivial if the subgraph it induces is empty or complete, that is, if s is an independent set or a clique of G. · Erdos1037.IsTrivialSet

IsTrivialUnit def

A unit in K[G] is trivial if it is exactly of the form kg where: - k is a unit in the base field K - g is an element of the group G · Kaplansky.IsTrivialUnit

IsTrivialZhaoSolution def

A solution $(x, y, z, x', y', z')$ of $x + 2y + 3z = x' + 2y' + 3z'$ is trivial if for every value $a$ the coefficients of the variables equal to $a$ have the same sum on both sides. · Green16.IsTrivialZhaoSolution

IsTuranConfiguration def

The configuration described by Tijdeman: if n is odd then the z i are exactly the nth roots of unity, and if n is even then they are the vertices of two regular (n / 2)-gons with the same circumscribed circle centred at the … · Erdos974.IsTuranConfiguration

IsTwinPrime def

A twin prime is a prime number that has a prime gap of 2, meaning either p - 2 or p + 2 is also prime. · DubnerConjecture.IsTwinPrime

IsTwoIndependent def

A vertex set is 2-independent when its induced graph has maximum degree at most one. · SimpleGraph.IsTwoIndependent

IsUInvariant def

IsUInvariant n means that some field of characteristic not 2 has $u$-invariant $n$, i.e. $n$ is the largest dimension of an anisotropic quadratic form over that field. · KaplanskyUInvariant.IsUInvariant

IsUlamSequence def

IsUlamSequence a means that $a$ is the Ulam sequence (OEIS A002858): $a(0) = 1$, $a(1) = 2$, and for each $n \geq 2$, $a(n)$ is the least integer greater than $a(n-1)$ that has a unique representation as $a(i) + a(j)$ with $i < j < n$. · Erdos342.IsUlamSequence

IsUltimatelyPeriodic def

A sequence $f : \mathbb{N} \to \mathbb{N}$ is ultimately periodic if there exist $N, P \in \mathbb{N}$, with $P>0$, such that for all $n \ge N$, $f(n+P) = f(n)$. · OeisA100475.IsUltimatelyPeriodic

IsUnbiased def

Two unitary matrices represent mutually unbiased bases if every entry of the relative unitary has squared norm $1 / d$. · OpenQuantumProblem13.IsUnbiased

IsUnderapprox def

S is an Egyptian underapproximation of x: valid denominators (all positive) and sum < x. · Erdos206.IsUnderapprox

IsUniform def

Every edge has exactly r vertices. · Finset.IsUniform

IsUniform def

Every edge has exactly k vertices. · Hypergraph.IsUniform

IsUniformOnSupport def

True if a PMF on $\mathbb{Z}$ is uniformly distributed on its support. · Green28.IsUniformOnSupport

IsUnimodalOnPrimes def

A function on the primes is unimodular if it first increases in $p$ until its maximum then decreases. · Erdos690.IsUnimodalOnPrimes

IsUnionClosed abbrev

abbrev IsUnionClosed (A : Finset (Finset n)) : Prop · UnionClosed.IsUnionClosed

IsUnionOfNIntervals def

A set $A \subseteq \mathbb{R}$ is a union of $n$ intervals if it can be written as $A = \bigcup_{i=1}^{n} (a_i, b_i)$ with $a_1 < b_1 < a_2 < b_2 < \dots < a_n < b_n$, i.e., as a disjoint union of $n$ nondegenerate open intervals in … · WeakTiling.IsUnionOfNIntervals

IsUniqueSubgraph def

G is a unique subgraph of H if there is exactly one subgraph of H isomorphic to G. Subgraphs of H are taken in the spanning sense: elements G' ≤ H of the lattice SimpleGraph V, i.e. subsets of the edges of H (not … · SimpleGraph.IsUniqueSubgraph

IsUnitaryPerfect def

A number $n > 0$ is a unitary perfect number if it is the sum of its proper unitary divisors. · Erdos1052.IsUnitaryPerfect

IsUnitEquilateralTriangle def

A unit equilateral triangle in Euclidean d-space. · Erdos755.IsUnitEquilateralTriangle

IsUnitIntervalDensity def

A nonnegative integrable function on $[0,1]$ with total integral $1$. · Green35.IsUnitIntervalDensity

IsUnivalentNormalized structure

The standard class $\mathcal{S}$ of normalised univalent functions on $\mathbb{D}$. · BrennanConjecture.IsUnivalentNormalized

IsValid def

A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is valid if no circle whose centre is one of the $x_i$ contains three other points. · Erdos655.IsValid

IsValidBlockConfig def

Check validity of block collection (disjoint and sensitive), A collection of blocks cB is valid for f at x if the blocks are disjoint and flipping any block changes f(x). · StrongSensitivityConjecture.IsValidBlockConfig

IsValidCollection def

A collection of intervals as in Erdős Problem 363: disjoint intervals of positive integers, each of size at least 4, whose product is a square. Intervals containing 0 are excluded, since their product is 0, which is a square. · Erdos363.IsValidCollection

IsValidMod def

A is valid mod N when the all-ones multiset is the only multiset of size #A drawn from A whose sum matches ∑ a ∈ A, a. · Arxiv.«2607.08366».IsValidMod

IsValidZerolessPower def

A helper predicate: $b^n$ is a power with base $>1$ whose decimal representation does not contain the digit 0. We assume $n$ is the exponent, $n \ge 1$. · OeisA103662.IsValidZerolessPower

IsVectorBundleWithRank class

A class for vector bundles of constant finite rank. · SheafOfModules.IsVectorBundleWithRank

IsWallSunSunPrime structure

Wall–Sun–Sun prime A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number. · IsWallSunSunPrime

IsWeakGiuga def

A (weak) Giuga number is a composite number $n$ such that $$\sum_{i=1}^{n - 1}i^{\varphi(n)} \equiv -1\pmod{n}$$. · AgohGiuga.IsWeakGiuga

IsWeakIrrationalitySequence def

The nondecreasing version of IsIrrationalitySequence, as used by Koizumi [Ko25]: the sequence is positive and nondecreasing, and every positive sequence asymptotic to it has irrational reciprocal sum. · Erdos263.IsWeakIrrationalitySequence

IsWeaklyBehrend def

A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$. · Erdos26.IsWeaklyBehrend

IsWeakMulBasis def

A weak additive basis of some order. · Set.IsWeakMulBasis

IsWeakMulBasisOfOrder def

def IsWeakMulBasisOfOrder (A : Set M) (n : ℕ) : Prop · Set.IsWeakMulBasisOfOrder

IsWeakTilingMeasure def

A positive, locally finite Borel measure $\nu$ on $\mathbb{R}$ is a weak tiling measure for a bounded measurable set $\Omega \subset \mathbb{R}$ if the convolution $1_\Omega \ast \nu = 1_{\Omega^c}$ holds almost everywhere, i.e., $\int … · WeakTiling.IsWeakTilingMeasure

IsWeightedTribonacci def

def IsWeightedTribonacci (a b c : ℤ) (x : ℕ → ℤ) : Prop · OeisA103425.IsWeightedTribonacci

IsWellDistributed def

Call $x_1,x_2,\ldots \in (0,1)$ well-distributed if, for every $\epsilon>0$, if $k$ is sufficiently large then, for all $n>0$ and intervals $I\subseteq [0,1]$, $\lvert \# \{ n < m\leq n+k : x_m\in I\} - \lvert I\rvert k\rvert < \epsilon k.$ · Erdos997.IsWellDistributed

IsWellTotallyDominated def

A graph G is well totally dominated if every minimal total dominating set has the same cardinality. · SimpleGraph.IsWellTotallyDominated

IsWieferichPrime abbrev

Wieferich prime A Wieferich prime is a prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $2$. · IsWieferichPrime

IsWieferichPrimeBase structure

Wieferich prime to base a A prime $p$ is a Wieferich prime to base $a$ if $p^2 \mid a^{p-1} - 1$, i.e. if $a^{p-1} \equiv 1 \pmod{p^2}$. · IsWieferichPrimeBase

IsWilsonPrime def

A Wilson prime is a prime $p$ such that $p^2 \mid (p-1)!+1$. · WilsonPrime.IsWilsonPrime

IsWolstenholmePrime def

A prime $p > 7$ is called a Wolstenholme prime if $\binom{2p-1}{p-1} \equiv 1 (\pmod{p^4})$. · WolstenholmePrime.IsWolstenholmePrime

IsZeroForcingSet def

A set $S$ is a zero forcing set of $G$ if its zero forcing closure is all of $V$. · Arxiv.«2507.17780».IsZeroForcingSet

IsZeroOne def

The predicate that all coefficients of a polynomial are either zero or one. P.coeffs is the finite set of all nonzero coefficients of the polynomial P. So IsZeroOne P means that every nonzero coefficient of P is equal to 1. Note … · Mathoverflow339137.IsZeroOne

IsZFinite def

m is Z-finite: it is annihilated by an ideal of Z of finite codimension over k. This is condition (c), with Z the centre of the universal enveloping algebra of the complexified Lie algebra of G(ℝ), i.e. … · AutomorphicForm.IsZFinite

IsZNumber def

A Z-number is a positive real number ξ such that the fractional part of ξ (3/2)^n lies in [0, 1/2) for every positive integer n. · IsZNumber

iteratedLog def

The iterated logarithm of a natural number in base b: the number of times Nat.log b must be iteratively applied to n before the result is at most 1. · Nat.iteratedLog

iteratedLog def

The iterated logarithm of x is the number of times the natural logarithm must be iteratively applied before the result is less than or equal to 1. Reference: https://en.wikipedia.org/wiki/Iterated_logarithm · Real.iteratedLog