Commit 2023-03-01 10:14 a0a7b109

View on Github →

feat: Port Algebra.Algebra.Tower (#2548)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Tower.lean

added theorem AlgEquiv.coe_restrictScalars

added theorem AlgEquiv.coe_restrict_scalars'

added def AlgEquiv.restrictScalars

added theorem AlgEquiv.restrictScalars_apply

added theorem AlgEquiv.restrictScalars_injective

added theorem AlgHom.coe_restrictScalars

added theorem AlgHom.coe_restrict_scalars'

added def AlgHom.restrictScalars

added theorem AlgHom.restrictScalars_apply

added theorem AlgHom.restrictScalars_injective

added def Algebra.lsmul

added theorem Algebra.lsmul_coe

added theorem Algebra.lsmul_injective

added theorem IsScalarTower.AlgHom.comp_algebraMap_of_tower

added theorem IsScalarTower.AlgHom.map_algebraMap

added theorem IsScalarTower.Algebra.ext

added theorem IsScalarTower.algebraMap_apply

added theorem IsScalarTower.algebraMap_eq

added theorem IsScalarTower.algebraMap_smul

added theorem IsScalarTower.coe_toAlgHom

added theorem IsScalarTower.coe_to_alg_hom'

added theorem IsScalarTower.of_algebraMap_eq'

added theorem IsScalarTower.of_algebraMap_eq

added def IsScalarTower.toAlgHom

added theorem IsScalarTower.toAlgHom_apply

added theorem Submodule.coe_span_eq_span_of_surjective

added theorem Submodule.map_mem_span_algebraMap_image

added theorem Submodule.restrictScalars_span

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_algebraMap_image

added theorem Submodule.span_algebraMap_image_of_tower

added theorem Submodule.span_smul_of_span_eq_top