Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 09:33 b4d4d9aa

View on Github →

feat(ring_theory/algebra): more on restrict_scalars (#2445)

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/data/complex/module.lean

Modified src/ring_theory/algebra.lean

added def algebra.restrict_scalars_equiv

added theorem algebra.restrict_scalars_equiv_apply

added theorem algebra.restrict_scalars_equiv_symm_apply

modified def linear_map.restrict_scalars

added theorem linear_map_algebra_module.smul_apply

added def module.restrict_scalars'

modified def module.restrict_scalars

added theorem module.restrict_scalars_smul_def

added theorem restrict_scalars_ker

added def submodule.restrict_scalars

added theorem submodule.restrict_scalars_bot

added theorem submodule.restrict_scalars_mem

added theorem submodule.restrict_scalars_top