Commit 2022-12-07 18:26 ed5ef408

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 Zulip thread.