Commit 2025-12-15 10:15 7e8c2cb6

feat(Algebra): prerequisites for #31919 (#32118)

• Extract a lemma exists_aeval_invOf_eq_zero_of_ideal_map_adjoin_add_span_eq_top that was used in the proof of [stacks#00IB](https://stacks.math.columbia.edu/tag/00IB) and are used to prove both parts of [stacks#090P](https://stacks.math.columbia.edu/tag/090P)
• Add lemmas on units in a submonoid of a DivisionMonoid/Group(WithZero)
• Add instances for integralClosure and API for integrally closed subrings
• Add a lemma on trailingCoeff of polynomials
• Fix a statement in local_hom_TFAE and rename to isLocalHom_tfae
• Unify the instances Algebra.ofSubsemiring and Algebra.ofSubring
• Move NonUnitalSub(semi)ringClass instance on Ideal to from Ideal/Operations to Defs
• Upgrade ValuationSubring.nonunits from Subsemigroup to NonUnitalSubring