English
Let f and g be polynomials over a base ring R, with hfg saying f equals g. Then the isomorphism between AdjoinRoot f and AdjoinRoot g induced by f = g sends the root of f to the root of g.
Русский
Пусть f и g — полиномы над R, и пусть hfg выражает равенство f = g. Тогда изоморфизм между AdjoinRoot f и AdjoinRoot g, индуцируемый равенством, отправляет корень f в корень g.
LaTeX
$$$\\\\operatorname{algEquivOfEq}(f,g,hfg)(\\\\sqrt[ AdjoinRoot f ]{root\_f}) = \\\\sqrt[ AdjoinRoot g ]{root\_g}$$$
Lean4
/-- `algEquivOfEq` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`. -/
theorem algEquivOfEq_root (f g : R[X]) (hfg) : algEquivOfEq f g hfg (root f) = root g := by
rw [coe_algEquivOfEq, algHomOfDvd_root]
