Real algebraic geometry: sign determination and cylindrical decomposition

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremValidity of Lazard's projection#

Every finite family of real polynomials in n variables has a cylindrical algebraic decomposition of ℝ ^ n into analytic submanifolds on each cell of which every member has constant Lazard valuation, when the coordinates are read in reverse order, from the coordinate added first by the cylindrical structure to the one added last. Every member is also sign-invariant on each cell. No well-orientedness hypothesis is imposed, and members may be nullified over base cells of positive dimension.

TauCeti.exists_isCAD_lazardValuationReindex_eq {n : ℕ} (F : Finset (MvPolynomial (Fin n) ℝ)) :
  ∃ 𝓒,
    TauCeti.IsCAD n 𝓒 ∧
      (∀ E ∈ 𝓒, ∃ d, TauCeti.IsAnalyticSubmanifold d E) ∧
        (∀ f ∈ F,
            ∀ E ∈ 𝓒,
              ∀ x ∈ E,
                ∀ y ∈ E,
                  f.lazardValuationReindex Fin.revPerm x = f.lazardValuationReindex Fin.revPerm y) ∧
          ∀ f ∈ F, ∀ E ∈ 𝓒, TauCeti.SignInvariant (fun x => (MvPolynomial.eval x) f) E
Lean

Formalized in Tau Ceti as TauCeti.exists_isCAD_lazardValuationReindex_eq.

Sources
LeanTauCeti.exists_isCAD_lazardValuationReindex_eq
Uses 2
Proof usesCAD lifting by Lazard delineations in a reordered base · Lazard lifting of a family

TheoremCorrectness of McCallum's projection#

A finite family of real polynomials that is well-oriented in McCallum's sense has a cylindrical algebraic decomposition into analytic submanifolds, on each cell of which every member of the family has constant ambient order.

TauCeti.exists_isCAD_orderAt_eq_of_isMcCallumWellOriented {n : ℕ}
  (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ))
  {F : Finset (MvPolynomial (Fin n) ℝ)} (hF : TauCeti.IsMcCallumWellOriented polynomialGCD n F) :
  ∃ 𝒞,
    TauCeti.IsCAD n 𝒞 ∧
      (∀ E ∈ 𝒞, ∃ d, TauCeti.IsAnalyticSubmanifold d E) ∧
        ∀ f ∈ F, ∀ E ∈ 𝒞, ∀ y ∈ E, ∀ y' ∈ E, f.orderAt y = f.orderAt y'
Lean

Formalized in Tau Ceti as TauCeti.exists_isCAD_orderAt_eq_of_isMcCallumWellOriented.

Sources
LeanTauCeti.exists_isCAD_orderAt_eq_of_isMcCallumWellOriented
Uses 7 · Used by 1
Statement usesTauCeti.IsMcCallumWellOriented
Proof usesThe analytic implicit root theorem · Finset.IsSquarefreeBasis · Hadamard's lemma along a graph · Identity theorem on the real points · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Riemann extension theorem across a coordinate hyperplane
Used byRecursive sign-invariant McCallum correctness

TheoremRecursive sign-invariant McCallum correctness#

If the McCallum projection of a squarefree basis of F is well-oriented, there is a sign-invariant CAD for F with analytic cells. Its base CAD is order-invariant for that projection. No restriction is imposed on nullification of the top-level basis, including over positive-dimensional base cells.

TauCeti.exists_isCAD_signInvariant_of_isMcCallumWellOriented_projection {n : ℕ}
  (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ))
  {F : Finset (MvPolynomial (Fin (n + 1)) ℝ)} {B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))}
  (_hB : (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).IsSquarefreeBasis B)
  (_hproj :
    TauCeti.IsMcCallumWellOriented polynomialGCD n
      ((Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B)) :
  ∃ 𝒞,
    TauCeti.IsCAD (n + 1) 𝒞 ∧
      (∀ E ∈ 𝒞, ∃ d, TauCeti.IsAnalyticSubmanifold d E) ∧
        (∀ f ∈ F, ∀ E ∈ 𝒞, TauCeti.SignInvariant (fun x => (MvPolynomial.eval x) f) E) ∧
          ∀ q ∈ (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B,
            ∀ C ∈ Set.image Fin.tail '' 𝒞, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y
Lean

Formalized in Tau Ceti as TauCeti.exists_isCAD_signInvariant_of_isMcCallumWellOriented_projection.

Sources
LeanTauCeti.exists_isCAD_signInvariant_of_isMcCallumWellOriented_projection
Uses 8
Statement usesFinset.IsSquarefreeBasis · TauCeti.IsMcCallumWellOriented
Proof usesThe analytic implicit root theorem · Correctness of McCallum's projection · Hadamard's lemma along a graph · Identity theorem on the real points · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Riemann extension theorem across a coordinate hyperplane

TheoremExistence of adapted cylindrical algebraic decompositions#

For every finite set F of real polynomials in n variables there is a cylindrical algebraic decomposition of ℝ ^ n on each cell of which every member of F is sign-invariant.

TauCeti.exists_isCAD_signInvariant {n : ℕ} (F : Finset (MvPolynomial (Fin n) ℝ)) :
  ∃ 𝒞,
    TauCeti.IsCAD n 𝒞 ∧ ∀ f ∈ F, ∀ E ∈ 𝒞, TauCeti.SignInvariant (fun x => (MvPolynomial.eval x) f) E
Lean

Formalized in Tau Ceti as TauCeti.exists_isCAD_signInvariant.

Sources
LeanTauCeti.exists_isCAD_signInvariant
Uses 1 · Used by 3
Proof usesCauchy's bound on the symmetric power
Used byThe Tarski–Seidenberg theorem · Finite-fiber dimension theorem · The local Nash graph criterion

TheoremThe Tarski–Seidenberg theorem#

The projection of a semialgebraic subset of ℝ ^ (n + 1) forgetting the coordinate 0 is semialgebraic. So quantifier elimination, the identification of semialgebraic sets with definable sets, and the image and composition laws of semialgebraic functions, which assume HasSemialgebraicProjections, hold over ℝ unconditionally.

TauCeti.instHasSemialgebraicProjectionsReal : TauCeti.HasSemialgebraicProjections ℝ
Lean

Formalized in Tau Ceti as TauCeti.instHasSemialgebraicProjectionsReal.

Sources
LeanTauCeti.instHasSemialgebraicProjectionsReal
Uses 1 · Used by 6
Proof usesExistence of adapted cylindrical algebraic decompositions
Used byTarski's theorem for the real field · Finite-fiber dimension theorem · Nash implicit function theorem for systems · The local Nash graph criterion · The Nash implicit root theorem · The Nash inverse function theorem

TheoremQuantifier elimination, given projection closure#

Every formula of ordered rings whose free variables Sum.inl r are assigned the parameters r ∈ R is equivalent, for every assignment v of the remaining free variables, to a quantifier-free formula with parameters.

TauCeti.exists_isQF_realize_iff.{u_1, u_2} {R : Type u_1} [CommRing R]
  [FirstOrder.Ring.CompatibleRing R] [FirstOrder.Language.order.Structure R] [LinearOrder R]
  [IsOrderedAddMonoid R]
  [(FirstOrder.Language.ring.sum FirstOrder.Language.order).OrderedStructure R]
  [TauCeti.HasSemialgebraicProjections R] {σ : Type u_2}
  (φ : (FirstOrder.Language.ring.sum FirstOrder.Language.order).Formula (R ⊕ σ)) :
  ∃ ψ,
    FirstOrder.Language.BoundedFormula.IsQF ψ ∧
      ∀ (v : σ → R), φ.Realize (Sum.elim id v) ↔ ψ.Realize (Sum.elim id v)
Lean

Formalized in Tau Ceti as TauCeti.exists_isQF_realize_iff.

Sources
LeanTauCeti.exists_isQF_realize_iff

TheoremTarski's theorem for the real field#

A subset of σ → ℝ is semialgebraic if and only if it is definable with parameters in the field ℝ, that is, in the language of rings with its usual interpretation.

TauCeti.isSemialgebraic_iff_definable_ring_real.{u_2} {σ : Type u_2} {s : Set (σ → ℝ)} :
  TauCeti.IsSemialgebraic s ↔ Set.univ.Definable FirstOrder.Language.ring s
Lean

Formalized in Tau Ceti as TauCeti.isSemialgebraic_iff_definable_ring_real.

Other forms

Tarski's theorem in the field language. Formalized in Tau Ceti as TauCeti.isSemialgebraic_iff_definable_ring.

TauCeti.isSemialgebraic_iff_definable_ring.{u_1, u_2} {R : Type u_1} [Field R]
  [FirstOrder.Ring.CompatibleRing R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R]
  {σ : Type u_2} [TauCeti.HasSemialgebraicProjections R] {s : Set (σ → R)} :
  TauCeti.IsSemialgebraic s ↔ Set.univ.Definable FirstOrder.Language.ring s
Sources
LeanTauCeti.isSemialgebraic_iff_definable_ring_real · TauCeti.isSemialgebraic_iff_definable_ring
Uses 1
Proof usesThe Tarski–Seidenberg theorem

TheoremAnalytic delineability from constant discriminant order#

A polynomial with nonzero fibers of constant degree over a preconnected analytic submanifold, whose nonzero formal discriminant has constant ambient order on the base, has a global delineation with intrinsically analytic root functions. Each root function is represented by an ambient function whose values off the base are immaterial. Along each root section, the polynomial, viewed as a polynomial in all n + 1 variables, has constant ambient order of vanishing.

No preservation of the formal degree or nonvanishing of the discriminant values is required. Multiple roots are allowed, and their fiber multiplicities are constant.

TauCeti.exists_analytic_delineation_of_orderAt_discr_eq {n d : ℕ} {S : Set (Fin n → ℝ)}
  {p : Polynomial (MvPolynomial (Fin n) ℝ)} (hS : TauCeti.IsAnalyticSubmanifold d S)
  (hconn : IsPreconnected S) (hp : ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) p ≠ 0)
  (hdegree :
    ∀ x ∈ S,
      ∀ y ∈ S,
        (Polynomial.map (MvPolynomial.eval x) p).natDegree =
          (Polynomial.map (MvPolynomial.eval y) p).natDegree)
  (hdiscr : p.discr ≠ 0) (horder : ∀ x ∈ S, ∀ y ∈ S, p.discr.orderAt x = p.discr.orderAt y) :
  ∃ D,
    (∀ (i : Fin D.count),
        ∃ r, TauCeti.AnalyticOnSubmanifold d r S ∧ ∀ (x : ↑S), r ↑x = D.root i x) ∧
      ∀ (i : Fin D.count) (x y : ↑S),
        ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (D.root i x) ↑x) =
          ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (D.root i y) ↑y)
Lean

Formalized in Tau Ceti as TauCeti.exists_analytic_delineation_of_orderAt_discr_eq.

Sources
LeanTauCeti.exists_analytic_delineation_of_orderAt_discr_eq
Uses 5
Proof usesThe analytic implicit root theorem · Hadamard's lemma along a graph · Identity theorem on the real points · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Riemann extension theorem across a coordinate hyperplane

StructureFinset.IsSquarefreeBasis#

B is a squarefree basis of the finite family F of polynomials over D: its members are primitive, squarefree, of positive degree and pairwise relatively prime, and every member of F is a constant times a product of powers of members of B.

Finset.IsSquarefreeBasis.{u_1} {D : Type u_1} [CommRing D] (F B : Finset (Polynomial D)) : Prop
Lean

Formalized in Tau Ceti as Finset.IsSquarefreeBasis.

Sources
LeanFinset.IsSquarefreeBasis
Used by 5
Used byCorrectness of McCallum's projection · Lazard lifting of a family · Recursive sign-invariant McCallum correctness · Sign-invariance of the McCallum projection does not suffice for lifting · TauCeti.IsMcCallumWellOriented

DefinitionTauCeti.IsMcCallumWellOriented#

A finite family F of real polynomials in n variables is well-oriented in McCallum's sense if, when n is positive, singling out the distinguished variable X 0 gives a family with a squarefree basis B such that each member of B is nullified at only finitely many points of ℝ ^ (n - 1), and the McCallum projection of the family with respect to B is again well-oriented. Every family of constants is well-oriented.

TauCeti.IsMcCallumWellOriented
  (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) (n : ℕ) :
  Finset (MvPolynomial (Fin n) ℝ) → Prop
Lean

Formalized in Tau Ceti as TauCeti.IsMcCallumWellOriented.

Sources
LeanTauCeti.IsMcCallumWellOriented
Uses 1 · Used by 2
Statement usesFinset.IsSquarefreeBasis
Used byCorrectness of McCallum's projection · Recursive sign-invariant McCallum correctness

TheoremMcCallum lifting fails over positive-dimensional nullifying cells#

The hypothesis of TauCeti.exists_isSemialgebraicStack_orderAt_eq_of_mcCallumProjection that no basis member is nullified over a cell with more than one point cannot be dropped, even over a connected semialgebraic analytic submanifold on which the McCallum projection is order-invariant.

Explicitly, let f = X₂ (X₀ + 1) + X₃ X₁, a polynomial in the distinguished variable X₀ and the base coordinates X₁, X₂, X₃, and let C ⊆ ℝ ^ 3 be the line of base points x with x₁ = x₂ = 0. As a polynomial in X₀, f is linear with coprime coefficients X₂ and X₂ + X₃ X₁, each of which vanishes to order one at every point of C; its content and discriminant are units. So for every irreducible basis B of {f}, every element of the McCallum projection has constant order on C, while every member of B is nullified over C. But f has order at least two at the point (-1, 0, 0, 0) above C, and order one at every point above C where X₀ ≠ -1 or X₁ ≠ 0. Since every cell of a stack over C lies over the whole of C, no stack over C, given by pointwise strictly increasing functions, continuous or not, has f order-invariant on each cell.

TauCeti.exists_nullified_mcCallumProjection_orderAt_ne
  (polynomialGCD : NormalizedGCDMonoid (MvPolynomial (Fin 3) ℝ)) :
  have this := polynomialGCD;
  ∃ f C,
    TauCeti.IsSemialgebraic C ∧
      TauCeti.IsAnalyticSubmanifold 1 C ∧
        IsConnected C ∧
          ∀ (B : Finset (Polynomial (MvPolynomial (Fin 3) ℝ))),
            (Finset.map (MvPolynomial.finSuccEquiv ℝ 3).toEmbedding {f}).IsIrreducibleBasis B →
              (∀
                  q ∈
                    (Finset.map (MvPolynomial.finSuccEquiv ℝ 3).toEmbedding {f}).mcCallumProjection
                      B,
                  ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y) ∧
                (∀ b ∈ B, ∀ x ∈ C, Polynomial.map (MvPolynomial.eval x) b = 0) ∧
                  ∀ (k : ℕ) (θ : Fin k → ↑C → ℝ),
                    (∀ (x : ↑C), StrictMono fun i => θ i x) →
                      ∃ E ∈ TauCeti.stackCells C θ, ∃ y ∈ E, ∃ y' ∈ E, f.orderAt y ≠ f.orderAt y'
Lean

Formalized in Tau Ceti as TauCeti.exists_nullified_mcCallumProjection_orderAt_ne.

Sources
LeanTauCeti.exists_nullified_mcCallumProjection_orderAt_ne

TheoremSign-invariance of the McCallum projection does not suffice for lifting#

In Finset.IsSquarefreeBasis.exists_isSemialgebraicStack_signInvariant_of_mcCallumProjection, the hypothesis that the McCallum projection is order-invariant on the base cannot be weakened to sign-invariance, even for a nonnullified squarefree basis over a connected semialgebraic analytic submanifold. So a lower level of a CAD that is merely sign-invariant for the projection cannot replace an order-invariant one.

Explicitly, let f = (T - 1)² (T - 1 - x₀²) + x₁, a monic cubic in the distinguished variable T over ℝ[x₀, x₁], and let S ⊆ ℝ ^ 2 be the line x₁ = 0. As f is squarefree, it is its own squarefree basis. Over S its coefficients 1, -(3 + x₀²), 3 + 2 x₀² and -(1 + x₀²) have constant signs, its content is 1, and its discriminant vanishes, because each fibre (T - 1)² (T - 1 - x₀²) has a double root. So the McCallum projection of {f} is sign-invariant on S, and some member of it has nonconstant order on S; since the other members do not vanish on S, this is the discriminant. But the fibre has the two roots 1 and 2 over (1, 0) and the single root 1 over the origin. In the coordinates (T, x₀, x₁), every cell of a stack over S lies over all of S, so the cells through the zeros (1, 1, 0) and (2, 1, 0) of f would both contain its only zero (1, 0, 0) over the origin, hence coincide, and then also contain (3 / 2, 1, 0), where f is negative. So no stack over S, given by pointwise strictly increasing functions, continuous or not, has f sign-invariant on each cell.

TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant
  (polynomialGCD : NormalizedGCDMonoid (MvPolynomial (Fin 2) ℝ)) :
  ∃ f S,
    {f}.IsSquarefreeBasis {f} ∧
      TauCeti.IsSemialgebraic S ∧
        TauCeti.IsAnalyticSubmanifold 1 S ∧
          IsConnected S ∧
            (∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) f ≠ 0) ∧
              (∀ q ∈ {f}.mcCallumProjection {f},
                  TauCeti.SignInvariant (fun x => (MvPolynomial.eval x) q) S) ∧
                (∃ q ∈ {f}.mcCallumProjection {f}, ∃ x ∈ S, ∃ y ∈ S, q.orderAt x ≠ q.orderAt y) ∧
                  ∀ (k : ℕ) (θ : Fin k → ↑S → ℝ),
                    (∀ (x : ↑S), StrictMono fun i => θ i x) →
                      ∃ E ∈ TauCeti.stackCells S θ,
                        ¬TauCeti.SignInvariant
                            (fun y =>
                              (MvPolynomial.eval y) ((MvPolynomial.finSuccEquiv ℝ 2).symm f))
                            E
Lean

Formalized in Tau Ceti as TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant.

Sources
LeanTauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant
Uses 6
Statement usesFinset.IsSquarefreeBasis
Proof usesThe analytic implicit root theorem · Hadamard's lemma along a graph · Identity theorem on the real points · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Riemann extension theorem across a coordinate hyperplane

TheoremLazard lifting of a family#

Over a preconnected analytic submanifold on which the Lazard projection of a family with respect to an irreducible basis is valuation-invariant, the family has a Lazard delineation. Its members may be nullified at points of the base.

TauCeti.nonempty_lazardDelineation_of_lazardProjection {n d : ℕ}
  [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)]
  {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)}
  (hB : F.IsIrreducibleBasis B) (hS : TauCeti.IsAnalyticSubmanifold d S) (hconn : IsPreconnected S)
  (hproj :
    ∀ q ∈ F.lazardProjection B, ∀ x ∈ S, ∀ y ∈ S, q.lazardValuation x = q.lazardValuation y) :
  Nonempty
    (TauCeti.LazardDelineation
      (fun f =>
        (MvPolynomial.rename ⇑finSuccEquivLast.symm)
          ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑f))
      S)
Lean

Formalized in Tau Ceti as TauCeti.nonempty_lazardDelineation_of_lazardProjection.

Sources
LeanTauCeti.nonempty_lazardDelineation_of_lazardProjection
Uses 6 · Used by 1
Proof usesThe analytic implicit root theorem · Finset.IsSquarefreeBasis · Hadamard's lemma along a graph · Identity theorem on the real points · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Riemann extension theorem across a coordinate hyperplane
Used byValidity of Lazard's projection

TheoremCAD lifting by Lazard delineations in a reordered base#

Suppose every cell C of a cylindrical algebraic decomposition of ℝ ^ n is an analytic submanifold, and its reordering (· ∘ e.symm) ⁻¹' C by a permutation e of the base coordinates carries a Lazard delineation of a fixed polynomial family. Then the stacks of those delineations, pulled back to the original cells, form a cylindrical algebraic decomposition of ℝ ^ (n + 1) with the original decomposition as its projection.

Every lifted cell is an analytic submanifold. On it, every family member has constant Lazard valuation when the base coordinates are read through e and the new coordinate is read last.

TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation_reindex.{u_1} {n : ℕ}
  {ι : Type u_1} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {𝓓 : Set (Set (Fin n → ℝ))}
  (h𝓓 : TauCeti.IsCAD n 𝓓) (e : Equiv.Perm (Fin n))
  (hanalytic : ∀ C ∈ 𝓓, ∃ d, TauCeti.IsAnalyticSubmanifold d C)
  (hD : ∀ C ∈ 𝓓, Nonempty (TauCeti.LazardDelineation F ((fun x => x ∘ ⇑(Equiv.symm e)) ⁻¹' C))) :
  ∃ 𝓒,
    TauCeti.IsCAD (n + 1) 𝓒 ∧
      Set.image Fin.tail '' 𝓒 = 𝓓 ∧
        (∀ E ∈ 𝓒, ∃ d, TauCeti.IsAnalyticSubmanifold d E) ∧
          ∀ (k : ι),
            ∀ E ∈ 𝓒,
              ∀ x ∈ E,
                ∀ y ∈ E,
                  (F k).lazardValuation (Fin.snoc (Fin.tail x ∘ ⇑e) (x 0)) =
                    (F k).lazardValuation (Fin.snoc (Fin.tail y ∘ ⇑e) (y 0))
Lean

Formalized in Tau Ceti as TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation_reindex.

Sources
LeanTauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation_reindex
Uses 1 · Used by 1
Proof usesThe analytic implicit root theorem
Used byValidity of Lazard's projection

DefinitionFinset.integerProjection#

The Collins projection of a finite family P of integer polynomials in the variables X 0, …, X n, computed over ℤ: single out the distinguished variable X 0 and take the Collins projection of the resulting family of polynomials in X 0 over ℤ[X 1, …, X n].

Finset.integerProjection {n : ℕ} (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
  Finset (MvPolynomial (Fin n) ℤ)
Lean

Formalized in Tau Ceti as Finset.integerProjection.

Sources
LeanFinset.integerProjection
Used by 1
Used byThe integer projection computes the real projection

TheoremThe integer projection computes the real projection#

Mapping the integer projection of P to ℝ gives the Collins projection of the real family of P.

Finset.image_map_integerProjection {n : ℕ} [DecidableEq (MvPolynomial (Fin n) ℝ)]
  (P : Finset (MvPolynomial (Fin (n + 1)) ℤ)) :
  Finset.image (⇑(MvPolynomial.map (Int.castRingHom ℝ))) P.integerProjection =
    P.integerFamily.collinsProjection
Lean

Formalized in Tau Ceti as Finset.image_map_integerProjection.

Sources
LeanFinset.image_map_integerProjection
Uses 1
Statement usesFinset.integerProjection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.