Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-13 19:42 050b8370

View on Github →

feat(field_theory/adjoin): Adjoin integral element (#4831)

Estimated changes

Modified src/data/finset/basic.lean

modified theorem multiset.disjoint_to_finset

added theorem multiset.to_finset_card_of_nodup

Modified src/field_theory/adjoin.lean

added theorem intermediate_field.adjoin_simple_to_subalgebra_of_integral

added theorem intermediate_field.card_alg_hom_adjoin_integral

Modified src/field_theory/fixed.lean