Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 10:15 70b14cee

View on Github →

refactor(*): use is_scalar_tower instead of restrict_scalars (#4733)

  • rename semimodule.restrict_scalars to restrict_scalars
  • rename restrict_scalars to subspace.restrict_scalars
  • use is_scalar_tower wherever possible
  • add warnings to docstrings about restrict_scalars to encourage is_scalar_tower instead

Estimated changes

added theorem algebra_map_smul
modified def linear_map.lto_fun
added theorem linear_map.smul_apply'
added def restrict_scalars
deleted theorem restrict_scalars_ker
deleted def smul_algebra_right
deleted theorem smul_algebra_right_apply
deleted def conjugate
deleted theorem conjugate_i
added theorem linear_map.conjugate_i
deleted def sum_of_conjugates