algebraMap_eq — Mathlib

English

The map algebraMap: R → AdjoinRoot f coincides with the inclusion map of R into the quotient AdjoinRoot f, i.e., algebraMap R (AdjoinRoot f) = of f.

Русский

Карта алгебры из R в AdjoinRoot f совпадает с вложением R в фактор-множество AdjoinRoot f: algebraMap R (AdjoinRoot f) = of f.

LaTeX

$$$\\text{algebraMap } R (AdjoinRoot f) = of f$$$

Lean4

@[simp]
theorem algebraMap_eq : algebraMap R (AdjoinRoot f) = of f :=
  rfl

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