English
If there is a suitable MulEquiv between root sets of M and N, then HasEnoughRootsOfUnity transfers from M to N.
Русский
Если существует подходящее взаимно однозначное гомоморфизм между множествами корней единицы M и N, то HasEnoughRootsOfUnity переносится с M на N.
LaTeX
$$MulEquiv.hasEnoughRootsOfUnity: e : rootsOfUnity n M ≃* rootsOfUnity n N → HasEnoughRootsOfUnity N n$$
Lean4
theorem hasEnoughRootsOfUnity {n : ℕ} [NeZero n] {M N : Type*} [CommMonoid M] [CommMonoid N]
[hm : HasEnoughRootsOfUnity M n] (e : rootsOfUnity n M ≃* rootsOfUnity n N) : HasEnoughRootsOfUnity N n
where
prim := by
obtain ⟨m, hm⟩ := hm.prim
use (e hm.toRootsOfUnity).val.val
rw [IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.coe_submonoidClass_iff]
refine .map_of_injective ?_ e.injective
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff]
cyc := isCyclic_of_surjective e e.surjective
