Commit 2020-12-31 06:04 b04aeb5e

View on Github →

chore(algebra): move lemmas from ring_theory.algebra_tower to algebra.algebra.tower (#5506) Moved some basic lemmas from ring_theory.algebra_tower to algebra.algebra.tower.

Estimated changes

Created src/algebra/algebra/tower.lean

added def algebra.lsmul

added theorem algebra.lsmul_coe

added theorem is_scalar_tower.algebra.ext

added theorem is_scalar_tower.algebra_comap_eq

added theorem is_scalar_tower.algebra_map_apply

added theorem is_scalar_tower.algebra_map_eq

added theorem is_scalar_tower.algebra_map_smul

added theorem is_scalar_tower.coe_restrict_base'

added theorem is_scalar_tower.coe_restrict_base

added theorem is_scalar_tower.coe_to_alg_hom'

added theorem is_scalar_tower.coe_to_alg_hom

added theorem is_scalar_tower.of_algebra_map_eq'

added theorem is_scalar_tower.of_algebra_map_eq

added theorem is_scalar_tower.range_under_adjoin

added def is_scalar_tower.restrict_base

added theorem is_scalar_tower.restrict_base_apply

added def is_scalar_tower.to_alg_hom

added theorem is_scalar_tower.to_alg_hom_apply

added theorem subalgebra.mem_res

added def subalgebra.of_under

added def subalgebra.res

added theorem subalgebra.res_inj

added theorem subalgebra.res_top

added theorem submodule.smul_mem_span_smul'

added theorem submodule.smul_mem_span_smul

added theorem submodule.smul_mem_span_smul_of_mem

added theorem submodule.span_smul

Modified src/ring_theory/algebra_tower.lean

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

deleted theorem subalgebra.mem_res

deleted def subalgebra.of_under

deleted def subalgebra.res

deleted theorem subalgebra.res_inj

deleted theorem subalgebra.res_top

deleted theorem submodule.smul_mem_span_smul'

deleted theorem submodule.smul_mem_span_smul

deleted theorem submodule.smul_mem_span_smul_of_mem

deleted theorem submodule.span_smul