Commit 2021-02-11 06:02 906e03de

chore(field_theory,ring_theory): reduce dependencies of power_basis.lean (#6104) I was having trouble with circular imports related to power_basis.lean, so I decided to reshuffle some definitions to make power_basis.lean have less dependencies. That way, something depending on power_basis doesn't also need to depend on intermediate_field.adjoin. The following (main) declarations are moved:

• algebra.adjoin: from ring_theory/adjoin.lean to ring_theory/adjoin/basic.lean (renamed file)
• algebra.adjoin.power_basis: from ring_theory/power_basis.lean to ring_theory/adjoin/power_basis.lean (new file)
• adjoin_root.power_basis: from ring_theory/power_basis.lean to ring_theory/adjoin_root.lean
• intermediate_field.adjoin.power_basis: from ring_theory/power_basis.lean to field_theory/adjoin.lean
• is_scalar_tower.polynomial: from ring_theory/algebra_tower.lean to ring_theory/polynomial/tower.lean (new file) The following results are new:
• is_integral.linear_independent_pow and is_integral.mem_span_pow: generalize algebra.adjoin.linear_independent_power_basis and algebra.adjoin.mem_span_power_basis.