Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-01 11:28 9af7e5b5

View on Github →

refactor(linear_algebra/basic): use smul_right (#1640)

refactor(linear_algebra/basic): use smul_right
Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison [email protected]
Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison [email protected]

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/mean_value.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_map.bound

deleted theorem continuous_linear_map.scalar_prod_space_iso_norm

added theorem continuous_linear_map.smul_right_norm

Modified src/linear_algebra/basic.lean

deleted def linear_map.scalar_prod_space_iso

modified theorem linear_map.sum_apply

Modified src/topology/algebra/module.lean

deleted def continuous_linear_map.scalar_prod_space_iso

added def continuous_linear_map.smul_right