Commit 2020-09-24 17:38 5c31dea2

View on Github →

feat(field_theory): intermediate fields (#4181) Define intermediate_field K L as a structure extending subalgebra K L and subfield L. This definition required some changes in subalgebra, which I added in #4180.

Estimated changes

Created src/field_theory/intermediate_field.lean

added theorem intermediate_field.add_mem

added theorem intermediate_field.algebra_map_mem

added theorem intermediate_field.coe_add

added theorem intermediate_field.coe_int_mem

added theorem intermediate_field.coe_inv

added theorem intermediate_field.coe_mul

added theorem intermediate_field.coe_neg

added theorem intermediate_field.coe_one

added theorem intermediate_field.coe_to_subalgebra

added theorem intermediate_field.coe_to_subfield

added theorem intermediate_field.coe_val

added theorem intermediate_field.coe_zero

added theorem intermediate_field.div_mem

added theorem intermediate_field.ext'

added theorem intermediate_field.ext

added theorem intermediate_field.field_range_le

added theorem intermediate_field.gsmul_mem

added theorem intermediate_field.inv_mem

added theorem intermediate_field.list_prod_mem

added theorem intermediate_field.list_sum_mem

added def intermediate_field.map

added theorem intermediate_field.mem_coe

added theorem intermediate_field.mem_mk

added theorem intermediate_field.mem_to_subalgebra

added theorem intermediate_field.mem_to_subfield

added theorem intermediate_field.mul_mem

added theorem intermediate_field.multiset_prod_mem

added theorem intermediate_field.multiset_sum_mem

added theorem intermediate_field.neg_mem

added theorem intermediate_field.one_mem

added theorem intermediate_field.pow_mem

added theorem intermediate_field.prod_mem

added theorem intermediate_field.set_range_subset

added theorem intermediate_field.smul_mem

added theorem intermediate_field.sub_mem

added theorem intermediate_field.sum_mem

added theorem intermediate_field.to_subalgebra_injective

added def intermediate_field.val

added theorem intermediate_field.val_mk

added theorem intermediate_field.zero_mem

added structure intermediate_field

added def subalgebra.to_intermediate_field

added def subfield.to_intermediate_field

Modified src/field_theory/subfield.lean

added theorem subfield.sub_mem

Modified src/ring_theory/algebra_tower.lean