Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-02 08:30 7310eab9

View on Github →

feat(field_theory/adjoin): adjoining elements to fields (#3913) Defines adjoining elements to fields

Estimated changes

Created src/field_theory/adjoin.lean

added theorem field.adjoin.algebra_map_mem

added theorem field.adjoin.mono

added theorem field.adjoin.range_algebra_map_subset

added def field.adjoin

added theorem field.adjoin_adjoin_left

added theorem field.adjoin_contains_field_as_subfield

added theorem field.adjoin_simple.algebra_map_gen

added def field.adjoin_simple.gen

added theorem field.adjoin_simple_adjoin_simple

added theorem field.adjoin_singleton

added theorem field.adjoin_subset_adjoin_iff

added theorem field.adjoin_subset_iff

added theorem field.adjoin_subset_subfield

added theorem field.mem_adjoin_simple_self

added theorem field.subfield_subset_adjoin_self

added theorem field.subset_adjoin

added theorem field.subset_adjoin_of_subset_left

added theorem field.subset_adjoin_of_subset_right

Modified src/ring_theory/algebra.lean

added theorem algebra.set_range_subset