Commit 2020-07-28 01:10 23bd09a8

View on Github →

chore(deprecated/ring): removing uses (#3577) This strips out a lot of the use of deprecated.ring. It's now only imported by data.polynomial.eval, and ring_theory.free_ring.

Estimated changes

Modified src/algebra/direct_limit.lean

modified theorem ring.direct_limit.of_pow

Modified src/algebra/group_power.lean

deleted theorem is_semiring_hom.map_pow

Modified src/algebra/group_with_zero.lean

Modified src/data/complex/exponential.lean

Modified src/data/equiv/ring.lean

deleted def ring_equiv.of'

deleted def ring_equiv.of

Modified src/data/mv_polynomial.lean

modified theorem mv_polynomial.is_id

modified def mv_polynomial.iter_to_sum

modified theorem mv_polynomial.map_eval₂

modified theorem mv_polynomial.map_id

modified theorem mv_polynomial.map_rename

modified def mv_polynomial.sum_to_iter

Modified src/data/polynomial/eval.lean

modified theorem polynomial.map_pow

Modified src/deprecated/group.lean

Modified src/deprecated/ring.lean

Modified src/field_theory/mv_polynomial.lean

Modified src/ring_theory/free_comm_ring.lean

added def free_ring.of'

Modified src/ring_theory/free_ring.lean

modified theorem free_ring.lift_comp_of

Modified src/ring_theory/integral_closure.lean

Modified src/ring_theory/subring.lean