English
Let R be a commutative ring. If f and g are polynomials in R[X] that are separable and coprime, then their product f g is separable.
Русский
Пусть R — коммутативный кольца. Если f и g — многочлены из R[X], являющиеся сепарабельными и взаимно простыми, то произведение f g сепарабельно.
LaTeX
$$$ \operatorname{Separable}(f) \land \operatorname{Separable}(g) \land \operatorname{IsCoprime}(f,g) \Rightarrow \operatorname{Separable}(f g)$$$
Lean4
theorem mul {f g : R[X]} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) : (f * g).Separable :=
by
rw [separable_def, derivative_mul]
exact ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)
