coe_toSemilinearMap — Mathlib

English

For any ring hom f: R →+* S, the underlying function of the semilinear map f.toSemilinearMap is exactly f itself; i.e., the function part coincides with f.

Русский

Для кольцевого гомоморфизма f: R →+* S функция, лежащая в основе семилинейного отображения f.toSemilinearMap, совпадает с f.

LaTeX

$$$\forall f: R \to+* S:\; (f^{\mathrm{toSemilinearMap}}) = f.$$$

Lean4

@[simp]
theorem _root_.RingHom.coe_toSemilinearMap (f : R →+* S) : ⇑f.toSemilinearMap = f :=
  rfl

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