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_equiv View on Github →