algebraMap_eq — Mathlib

English

The algebra map to ULift A is compatible with the ordinary algebra map to A via ULift’s projection; explicitly, algebraMap R (ULift A) r = ULift.up (algebraMap R A r).

Русский

Алгебраическое отображение в ULift A согласуется с обычным отображением в A: algebraMap_R (ULift A) r = ULift.up (algebraMap_R A r).

LaTeX

$$$\operatorname{algebraMap} R (\mathrm{ULift} A) r = \mathrm{ULift.up}(\operatorname{algebraMap} R A r)$$$

Lean4

theorem _root_.ULift.algebraMap_eq (r : R) : algebraMap R (ULift A) r = ULift.up (algebraMap R A r) :=
  rfl

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