English
Equivalence symmetry yields that the inverse maps α to the fixed root in the base field.
Русский
Симметрия эквив обеспечивает, что обратное отображение переводит α к фиксированному корню в базовом поле.
LaTeX
$$$(autAdjoinRootXPowSubCEquiv hζ H).symm α = \\mathrm{root}$$$
Lean4
theorem autAdjoinRootXPowSubCEquiv_symm_smul [NeZero n] (σ) :
((autAdjoinRootXPowSubCEquiv hζ H).symm σ : Kˣ) • (root _ : K[n√a]) = σ (root _) :=
by
have := Fact.mk H
simp only [autAdjoinRootXPowSubCEquiv, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MulEquiv.symm_mk, MulEquiv.coe_mk,
Equiv.coe_fn_symm_mk, AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, rootsOfUnity.mkOfPowEq,
Units.smul_def, Algebra.smul_def, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.val_ofPowEqOne, ite_mul,
one_mul]
simp_rw [← root_X_pow_sub_C_eq_zero_iff H]
split_ifs with h
· rw [h, map_zero]
· rw [div_mul_cancel₀ _ h]
