algEquivOfEq — Mathlib

English

If R is a domain and f is prime with nonzero degree, then NoZeroSMulDivisors(R, AdjoinRoot f).

Русский

Если R — область и f — простой многочлен ненулевой степени, то NoZeroSMulDivisors(R, AdjoinRoot f).

LaTeX

$$NoZeroSMulDivisors_R(AdjoinRoot f)$$

Lean4

/-- The canonical algebraic equivalence between `AdjoinRoot f` and `AdjoinRoot g`, where
the two polynomials `f g : R[X]` are equal. -/
noncomputable def algEquivOfEq (f g : R[X]) (hfg : f = g) : AdjoinRoot f ≃ₐ[R] AdjoinRoot g :=
  algEquivOfAssociated f g (by rw [hfg])

Похожие утверждения