Facts about regular functions

comp_aevallemma

Evaluation commutes with composition.

lemma comp_aeval (F : RegularFunction k σ τ) (G : RegularFunction k τ ι) (a : σ → k) :
    (F.comp G).aeval a = G.aeval (F.aeval a) := by
  ext i
  rw [aeval, comp, MvPolynomial.aeval_bind₁, ← aeval]
  rfl

Builds on

Regular function

Used by

Counterexample to the Jacobian conjecture in dimension three

import Conjectura.Theorems.Mathematics.AlgebraicGeometry.RegularFunction · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `FormalConjectures/Wikipedia/JacobianConjecture.lean`. Split into one concept per module; no mathematical content changed.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits