Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 11:21 2e1d8d67

View on Github →

feat(ring_theory/roots_of_unity): fun_like support (#11735)

feat(ring_theory/roots_of_unity): ring_hom_class
oops these could've been monoid homs from the start

Estimated changes

Modified src/field_theory/abel_ruffini.lean

Modified src/ring_theory/roots_of_unity.lean

modified theorem is_primitive_root.map_iff_of_injective

modified theorem is_primitive_root.map_of_injective

modified theorem is_primitive_root.of_map_of_injective

added theorem map_root_of_unity_eq_pow_self

added def restrict_roots_of_unity

added theorem restrict_roots_of_unity_coe_apply

deleted theorem ring_hom.map_root_of_unity_eq_pow_self

deleted def ring_hom.restrict_roots_of_unity

deleted theorem ring_hom.restrict_roots_of_unity_coe_apply