Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 04:51 51546d29

View on Github →

chore(ring_theory/free_ring): use bundled ring homs (#4011) Use bundled ring homs in free_ring and free_comm_ring.

Estimated changes

modified def free_comm_ring.lift
deleted theorem free_comm_ring.lift_add
modified theorem free_comm_ring.lift_comp_of
deleted theorem free_comm_ring.lift_mul
deleted theorem free_comm_ring.lift_neg
deleted theorem free_comm_ring.lift_one
deleted theorem free_comm_ring.lift_pow
deleted theorem free_comm_ring.lift_sub
deleted theorem free_comm_ring.lift_zero
deleted theorem free_comm_ring.map_add
deleted theorem free_comm_ring.map_mul
deleted theorem free_comm_ring.map_neg
deleted theorem free_comm_ring.map_one
deleted theorem free_comm_ring.map_pow
deleted theorem free_comm_ring.map_sub
deleted theorem free_comm_ring.map_zero
modified def free_ring.lift
deleted theorem free_ring.lift_add
deleted def free_ring.lift_hom
deleted theorem free_ring.lift_mul
deleted theorem free_ring.lift_neg
deleted theorem free_ring.lift_one
deleted theorem free_ring.lift_pow
deleted theorem free_ring.lift_sub
deleted theorem free_ring.lift_zero
modified def free_ring.map
deleted theorem free_ring.map_add
deleted def free_ring.map_hom
deleted theorem free_ring.map_mul
deleted theorem free_ring.map_neg
modified theorem free_ring.map_of
deleted theorem free_ring.map_one
deleted theorem free_ring.map_pow
deleted theorem free_ring.map_sub
deleted theorem free_ring.map_zero