Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 30195815

View on Github →

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.

Estimated changes

Modified src/field_theory/adjoin.lean

added theorem intermediate_field.adjoin_empty

added theorem intermediate_field.adjoin_eq_algebra_adjoin

added theorem intermediate_field.adjoin_insert_adjoin

deleted theorem intermediate_field.adjoin_le_algebra_adjoin

added theorem intermediate_field.eq_adjoin_of_eq_algebra_adjoin

added def intermediate_field.fg

added theorem intermediate_field.fg_adjoin_finset

added theorem intermediate_field.fg_bot

added theorem intermediate_field.fg_def

added theorem intermediate_field.fg_of_fg_to_subalgebra

added theorem intermediate_field.fg_of_noetherian

Modified src/field_theory/intermediate_field.lean

added theorem intermediate_field.to_subalgebra_le_to_subalgebra

added theorem intermediate_field.to_subalgebra_lt_to_subalgebra

Modified src/ring_theory/adjoin.lean

added theorem algebra.adjoin_insert_adjoin

added theorem subalgebra.fg_of_fg_to_submodule

added theorem subalgebra.fg_of_noetherian

added theorem subalgebra.induction_on_adjoin