id — Mathlib · SciLib

English

The algebra map from R to R is the identity map.

Русский

Алгебраическое отображение из R в R есть тождественное отображение.

LaTeX

$$$\operatorname{algebraMap}(R,R) = \mathrm{id}$$$

Lean4

/-- The identity map inducing an `Algebra` structure. -/
instance (priority := 1100) id : Algebra R R where
  -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot
    -- be made so without a significant performance hit.
    -- see library note [reducible non-instances].

  toSMul := Mul.toSMul _
  __ := ({ RingHom.id R with toFun x := x }).toAlgebra

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