mathlib
6734a730 - fix(*): Close unsolved `has_scalar R R`, `is_scalar_tower R R ↥M`, and `is_scalar_tower R R ↥N` goals

Commit

5 years ago

fix(*): Close unsolved `has_scalar R R`, `is_scalar_tower R R ↥M`, and `is_scalar_tower R R ↥N` goals

Author

eric-wieser

Parents