English
IsAdjoinRootMonic.basis is independent of the chosen representation; many equalities hold between coefficients when mapped via h.map and h.repr.
Русский
Основа IsAdjoinRootMonic.basis не зависит от выбора представления; выполняются равенства коэффициентов при отображении через h.map и h.repr.
LaTeX
$$$ h.basis = h.basis \text{ (in the appropriate representation context)} $$$
Lean4
/-- `IsAdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`. -/
def modByMonicHom : S →ₗ[R] R[X] where
toFun x := h.repr x %ₘ f
map_add' x y := by conv_lhs => rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]
map_smul' c
x := by
rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul, h.modByMonic_repr_map, ←
smul_eq_C_mul, smul_modByMonic, h.map_repr]
