Mathlib v3 is deprecated. Go to Mathlib v4

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