mathlib3

30195815 - feat({field,ring}_theory/adjoin): generalize `induction_on_adjoin` (#4647)

feat({field,ring}_theory/adjoin): generalize `induction_on_adjoin` (#4647) We can prove `induction_on_adjoin` for both `algebra.adjoin` and `intermediate_field.adjoin` in a very similar way, if we add a couple of small lemmas. The extra lemmas I introduced for `algebra.adjoin` shorten the proof of `intermediate_field.adjoin` noticeably.