Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 07:21 400dbb3a

View on Github →

refactor(ring_theory/non_zero_divisors): use fun_like (#11764)

Estimated changes

Modified src/field_theory/ratfunc.lean

Modified src/number_theory/cyclotomic/basic.lean

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/laurent_series.lean

Modified src/ring_theory/localization.lean

Modified src/ring_theory/non_zero_divisors.lean

added theorem map_le_non_zero_divisors_of_injective

added theorem map_mem_non_zero_divisors

added theorem map_ne_zero_of_mem_non_zero_divisors

added theorem mem_non_zero_divisors_of_ne_zero

deleted theorem monoid_with_zero_hom.map_le_non_zero_divisors_of_injective

deleted theorem monoid_with_zero_hom.map_mem_non_zero_divisors

deleted theorem monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors

added theorem non_zero_divisors_le_comap_non_zero_divisors_of_injective

deleted theorem ring_hom.map_le_non_zero_divisors_of_injective

deleted theorem ring_hom.map_mem_non_zero_divisors

deleted theorem ring_hom.map_ne_zero_of_mem_non_zero_divisors

Modified src/ring_theory/polynomial/scale_roots.lean