down_algebraMap — Mathlib

English

The projection of the algebra map to ULift A equals the algebra map to A: (algebraMap R (ULift A) r).down = algebraMap R A r.

Русский

Проекция алгебраического отображения в ULift A равна алгебраическому отображению в A: down(algebraMap_R (ULift A) r) = algebraMap_R A r.

LaTeX

$$$(\mathrm{algebraMap}\, R\ (\mathrm{ULift} A)\ r).down = \mathrm{algebraMap}\, R\ A\ r$$$

Lean4

@[simp]
theorem _root_.ULift.down_algebraMap (r : R) : (algebraMap R (ULift A) r).down = algebraMap R A r :=
  rfl

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