Commit 2025-08-06 17:32 fc65f32d

feat(Algebra/Adjoin): singleton as aeval (#27828) For x : A, elements of Algebra.adjoin R {x} can be represented as a polynomial of R evaluated at the point x. This PR introduces three (3) theorems related to this:

• adjoin_mem_exists_aeval rewrite an element of A in adjoin R {x} as the aeval of some polynomial.
• adjoin_eq_exists_aeval rewrite an element adjoin R {x} as the aeval of some polynomial.
• adjoin_singleton_induction: an induction principle reducing problems over adjoin R {x} to problems of the form M (⟨aeval x p, aeval_mem_adjoin_singleton R x⟩ : adjoin R {x}).