Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_monoid_hom.coe_to_real_linear_map

Modification history

2020-05-01 05:59

src/topology/instances/real_vector_space.lean

feat(topology/instances/real_vector_space): `E →+ F` to `E →L[ℝ] F` (#2577) …

Added add_monoid_hom.coe_to_real_linear_map View on Github →