aux_algebraMap — Mathlib

English

The auxiliary lifting map respects the algebra map on scalars: aux f maps algebraMap_R (even Q) r to algebraMap_R A r.

Русский

Вспомогательное подъемное отображение сохраняет алгебраическое отображение на скалярах: aux f отображает algebraMap_R (even Q) r в algebraMap_R A r.

LaTeX

$$aux_algebraMap: aux f (algebraMap R (even Q) r) = algebraMap R A r$$

Lean4

@[simp]
theorem aux_algebraMap (r) : aux f (algebraMap R (even Q) r) = algebraMap R A r :=
  (congr_arg Prod.fst (foldr_algebraMap _ _ _ _ _)).trans (Algebra.algebraMap_eq_smul_one r).symm

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