isAdjoinRootMonic_root_eq_root — Mathlib

English

If f is monic, then (AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f.

Русский

Если f моноическая, то корень из isAdjoinRootMonic совпадает с корнем AdjoinRoot.

LaTeX

$$$ (AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f $$$

Lean4

@[deprecated "Use `simp` instead" (since := "2025-08-07")]
theorem isAdjoinRootMonic_root_eq_root (hf : Monic f) : (AdjoinRoot.isAdjoinRootMonic f hf).root = AdjoinRoot.root f :=
  by simp

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