Commit 2025-11-25 06:59 ea3d89c5

feat(FieldTheory/IntermediateField/Adjoin): generates as a algebra iff generates as an intermediate field (#32028)

• Prove equivalence of a set of algebraic elements generating an algebra as an algebra and as an intermediate field
• Make assumptions in this section consistently assume IsAlgebraic rather than IsIntegral
• Make names consistent with naming convention
• Add simp lemma giving the underlying subalgebra of an intermediate field when it is generated by a set of algebraic elements