Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-24 07:49 d487d650

View on Github →

refactor(topology,algebraic_geometry): use bundled maps here and there (#10447)

  • opens.comap now takes a continuous_map and returns a preorder_hom;
  • prime_spectrum.comap is now a bundled continuous_map.

Estimated changes

modified def prime_spectrum.comap
modified theorem prime_spectrum.comap_id