val — Mathlib

English

Another articulation of compatibility between algebra maps from R' to S and from R' to A.

Русский

Другой способ выразить совместимость алгебраMap от R' к S и от R' к A.

LaTeX

$$$\uparrow(\mathrm{algebraMap}_{R'} S r) = \mathrm{algebraMap}_{R'} A r$$$

Lean4

/-- Embedding of a subalgebra into the algebra. -/
def val : S →ₐ[R] A :=
  { toFun := ((↑) : S → A)
    map_zero' := rfl
    map_one' := rfl
    map_add' := fun _ _ ↦ rfl
    map_mul' := fun _ _ ↦ rfl
    commutes' := fun _ ↦ rfl }

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