mathlib3
9851a886 - feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872)

Commit

5 years ago

feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872) I'm going to use these definitions to prove `times_cont_diff_at.restrict_scalars` etc.

References

#4925 - Make prime-avoidance branch build

Author

urkud

Parents

63d109fe

mathlib3 9851a886 - feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872)

mathlib3
9851a886 - feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872)