mathlib

ed5ef408 - feat(topology/algebra/uniform_ring): add dense_inducing.extend_hom (#17212)

feat(topology/algebra/uniform_ring): add dense_inducing.extend_hom (#17212) This PR adds some lemmas that will be used in the proof (#17285) that two complex embeddings of a field define the same place iff they are equal or complex conjugate: - `dense_inducing.extend_ring_hom` constructs a ring homomorphism out of `dense_inducing.extend` - `subfield.topological_closure` proves that the closure of a subfield in a topological division ring is also a subfield and also some additional useful lemmas about this closure similar to the ones existing for `subring` This PR also includes some slight modifications to files in `algebraic_geometry` to fix a timeout in CI, see [this](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Deterministic.20timeout.20in.20CI/near/307129547) Zulip thread.