Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 10:09 c444a005

View on Github →

Revert "chore(ring_theory): delete is_algebra_tower" This reverts commit c956ce1516ccfb3139ae3ebde7ede9c678d81968.

Estimated changes

Modified src/field_theory/algebraic_closure.lean

Modified src/field_theory/splitting_field.lean

Modified src/field_theory/tower.lean

Modified src/ring_theory/algebra.lean

Modified src/ring_theory/algebra_tower.lean

added theorem is_algebra_tower.aeval_apply

added theorem is_algebra_tower.algebra.ext

added theorem is_algebra_tower.algebra_map_apply

added theorem is_algebra_tower.algebra_map_eq

added theorem is_algebra_tower.algebra_map_smul

added theorem is_algebra_tower.comap_eq

added theorem is_algebra_tower.of_algebra_map_eq

added theorem is_algebra_tower.range_under_adjoin

added def is_algebra_tower.restrict_base

added theorem is_algebra_tower.restrict_base_apply

added theorem is_algebra_tower.smul_left_comm

added def is_algebra_tower.to_alg_hom

added theorem is_algebra_tower.to_alg_hom_apply

added def is_algebra_tower

deleted theorem is_scalar_tower.aeval_apply

deleted theorem is_scalar_tower.algebra.ext

deleted theorem is_scalar_tower.algebra_comap_eq

deleted theorem is_scalar_tower.algebra_map_apply

deleted theorem is_scalar_tower.algebra_map_eq

deleted theorem is_scalar_tower.algebra_map_smul

deleted theorem is_scalar_tower.of_algebra_map_eq

deleted theorem is_scalar_tower.range_under_adjoin

deleted def is_scalar_tower.restrict_base

deleted theorem is_scalar_tower.restrict_base_apply

deleted theorem is_scalar_tower.smul_left_comm

deleted def is_scalar_tower.to_alg_hom

deleted theorem is_scalar_tower.to_alg_hom_apply

Modified src/ring_theory/algebraic.lean

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_of_is_algebra_tower

deleted theorem is_integral_of_is_scalar_tower

Modified src/ring_theory/localization.lean

modified theorem fraction_map.comap_is_algebraic_iff