Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-18 13:48 542ff6af

View on Github →

refactor(algebra/algebra/basic): change submodule.restrict_scalars to use is_scalar_tower (#6745)

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem linear_map.ker_restrict_scalars

modified def submodule.restrict_scalars

modified theorem submodule.restrict_scalars_bot

modified theorem submodule.restrict_scalars_inj

modified theorem submodule.restrict_scalars_mem

modified theorem submodule.restrict_scalars_top

modified theorem submodule.span_le_restrict_scalars