mathlib
9b3ea03d - feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359)

Commit

3 years ago

feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359) I will wait for a later PR to (maybe) fix the reducibility/simp of these declarations.

Author

fpvandoorn

Parents

dba797a4

mathlib 9b3ea03d - feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359)

mathlib
9b3ea03d - feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359)