mathlib

mathlib copied to clipboard

Unbundled homomorphisms are deprecated but are still used in many files. Here is the output of git grep -l 'is_\(semi\)\?ring_hom' with my comments:

• src/algebra/direct_limit.lean
• src/algebra/field.lean :: only used for a few map_* lemmas.
• src/algebra/field_power.lean :: used for is_ring_hom.map_fpow.
• src/algebra/group_power.lean
• src/algebra/pi_instances.lean :: used for is_ring_hom_pi, fst.is_ring_hom, and snd.is_ring_hom
• src/algebra/pointwise.lean
• src/algebra/punit_instances.lean
• src/algebra/ring.lean :: definition etc
• src/data/complex/basic.lean :: we can redefine conj etc to be ring_homs or alg_homs but this way we loose z.conj notation
• src/data/equiv/ring.lean
• src/data/mv_polynomial.lean :: used for C, eval₂, eval, and map; I'm going to rewrite it using bundled homs once I'm done with polynomials
• src/data/padics/padic_integers.lean
• src/data/polynomial.lean :: migrating to bundled homs and aeval in #2492
• src/data/real/ennreal.lean :: see #2533
• src/data/real/nnreal.lean :: see #2533
• src/data/zsqrtd/gaussian_int.lean
• src/field_theory/minimal_polynomial.lean
• src/field_theory/mv_polynomial.lean
• ~~src/field_theory/subfield.lean:: see #2544~~
• src/ring_theory/adjoin_root.lean
• src/ring_theory/algebra_operations.lean
• src/ring_theory/free_comm_ring.lean
• src/ring_theory/free_ring.lean
• src/ring_theory/integral_closure.lean
• src/ring_theory/localization.lean :: waiting for a rewrite based on monoid_localization
• src/ring_theory/maps.lean
• src/ring_theory/power_series.lean
• src/topology/algebra/module.lean : see #2545
• src/topology/algebra/uniform_ring.lean

P.S. : git grep 'is_\(semi\)\?ring_hom' | wc -l returns 339