isAdjoinRootMonic — Mathlib

English

For monic f, AdjoinRootMonic map equals mk f: (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f.

Русский

Для моничного f, отображение isAdjoinRootMonic равно mk f: (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f.

LaTeX

$$$ (AdjoinRoot.isAdjoinRootMonic f hf).map = AdjoinRoot.mk f $$$

Lean4

/-- `AdjoinRoot f` is indeed given by adjoining a root of `f`. If `f` is monic this is more
powerful than `AdjoinRoot.isAdjoinRoot`. -/
protected def isAdjoinRootMonic (hf : Monic f) : IsAdjoinRootMonic (AdjoinRoot f) f
    where
  __ := AdjoinRoot.isAdjoinRoot f
  monic := hf

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