is_separable

Stream: general

[Sebastien Gouezel]

We have currently docs#is_separable (about field extensions) in the root namespace. I need to introduce topological_space.is_separable for sets with a countable dense subset, but then Lean complains all the time that the name is ambiguous. This would be solved by putting the field extension notion in a namespace that I wouldn't open. Does it make sense to you? What would be the natural namespace here?

[Kevin Buzzard]

ring_hom?

[Riccardo Brasca]

I would vote for algebra.is_separable (since it is currently stated for an algebra, not for a ring_hom).

[Riccardo Brasca]

And I have the impression I always have open algebra when working with this stuff, so in practice this shouldn't change a lot of proofs.