Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-13 09:00 b54960d1

View on Github →

refactor(*): migrate some files to bundled ring homs (#2133)

  • refactor(*): migrate some files to bundled ring homs
  • Rename ring_hom.is_local back to is_local_ring_hom
  • Apply suggestions from code review Co-Authored-By: Johan Commelin johan@commelin.net
  • Restore 2 instances, make map use bundled homs
  • More bundled homs
  • Add a docstring

Estimated changes

added theorem ring_hom.map_prod
added theorem ring_hom.map_sum
modified theorem ring.direct_limit.lift_add
modified theorem ring.direct_limit.lift_mul
modified theorem ring.direct_limit.lift_neg
modified theorem ring.direct_limit.lift_one
modified theorem ring.direct_limit.lift_pow
modified theorem ring.direct_limit.lift_sub
modified theorem ring.direct_limit.lift_zero
added theorem ring_hom.coe_mk
modified theorem adjoin_root.coe_injective
modified theorem adjoin_root.eval₂_root
modified theorem adjoin_root.is_root_root
modified def adjoin_root.lift
modified theorem adjoin_root.lift_mk
modified theorem adjoin_root.lift_of
modified theorem adjoin_root.lift_root
modified def adjoin_root.mk
added theorem adjoin_root.mk_C
modified theorem adjoin_root.mk_self
modified def adjoin_root.of
modified def adjoin_root.root
modified def adjoin_root
modified def free_comm_ring.map
modified theorem free_comm_ring.map_add
modified theorem free_comm_ring.map_mul
modified theorem free_comm_ring.map_neg
modified theorem free_comm_ring.map_of
modified theorem free_comm_ring.map_one
modified theorem free_comm_ring.map_pow
modified theorem free_comm_ring.map_sub
modified theorem free_comm_ring.map_zero
deleted theorem is_ring_hom.injective_iff
deleted def is_ring_hom.ker
deleted theorem is_ring_hom.ker_eq
deleted theorem is_ring_hom.ker_is_prime
deleted theorem is_ring_hom.mem_ker
added def ring_hom.ker
added theorem ring_hom.ker_eq
added theorem ring_hom.ker_is_prime
added theorem ring_hom.mem_ker
modified def ideal.quotient.lift
modified theorem ideal.quotient.lift_mk
added theorem ideal.quotient.mk_prod
added theorem ideal.quotient.mk_sum
modified theorem is_unit_of_map_unit