Mathlib v3 is deprecated. Go to Mathlib v4

Def add_equiv.to_real_linear_equiv

Modification history

2021-12-09 08:54
src/topology/instances/real_vector_space.lean
feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490) …
Added add_equiv.to_real_linear_equivView on Github →