Commit 2021-11-02 10:26 658a3d77

View on Github →

refactor(algebra/algebra): remove subalgebra.under (#10081) This removes subalgebra.under, and replaces subalgebra.of_under with subalgebra.of_restrict_scalars. Lemmas associated with under have been renamed accordingly.

Estimated changes

Modified src/algebra/algebra/tower.lean

added theorem is_scalar_tower.adjoin_range_to_alg_hom

deleted theorem is_scalar_tower.range_under_adjoin

deleted theorem subalgebra.mem_under

added def subalgebra.of_restrict_scalars

deleted def subalgebra.of_under

deleted def subalgebra.under

Modified src/field_theory/is_alg_closed/basic.lean

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_union_eq_adjoin_adjoin

deleted theorem algebra.adjoin_union_eq_under

Modified src/ring_theory/adjoin/fg.lean

Modified src/ring_theory/algebra_tower.lean