mathlib
ef7e8ddd - Instantiate `add_monoid_hom_class` for `continuous_linear_map`

Commit

4 years ago

Instantiate `add_monoid_hom_class` for `continuous_linear_map`

Author

Vierkantor

Vierkantor

Parents

Loading