mathlib3
16ad1b41 - chore(topology/basic): remove unneeded `mk_protected` (#2971)

Commit

5 years ago

chore(topology/basic): remove unneeded `mk_protected` (#2971) It was already fixed by adding `@[protect_proj]`.

Author

rwbarton

Parents