Commit 2021-03-08 12:32 5d0a40f1

View on Github →

feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars (#6548) This also renames is_scalar_tower.restrict_base to alg_hom.restrict_scalars, to enable dot notation and match linear_map.restrict_scalars.

Estimated changes

Modified src/algebra/algebra/basic.lean

added def alg_equiv.comap

modified def alg_hom.comap

Modified src/algebra/algebra/tower.lean

added theorem alg_equiv.coe_restrict_scalars'

added theorem alg_equiv.coe_restrict_scalars

added def alg_equiv.restrict_scalars

added theorem alg_equiv.restrict_scalars_apply

added theorem alg_hom.coe_restrict_scalars'

added theorem alg_hom.coe_restrict_scalars

added def alg_hom.restrict_scalars

added theorem alg_hom.restrict_scalars_apply

deleted theorem is_scalar_tower.coe_restrict_base'

deleted theorem is_scalar_tower.coe_restrict_base

deleted def is_scalar_tower.restrict_base

deleted theorem is_scalar_tower.restrict_base_apply

Modified src/field_theory/normal.lean

Modified src/ring_theory/algebra_tower.lean