mathlib

906e03de - chore(field_theory,ring_theory): reduce dependencies of `power_basis.lean` (#6104)

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`.