algebraMap_lift — Mathlib

English

The composition of algebra maps aligns with lift: algebraMap A B (lift x) = algebraMap S B x.

Русский

Составление алгебраических отображений согласуется с lift: algebraMap A B (lift x) = algebraMap S B x.

LaTeX

$$$\text{algebraMap } A B (\mathrm{lift} \ R \ A \ B \ x) = \text{algebraMap } S B x$$$

Lean4

@[simp]
theorem algebraMap_lift (x : S) : algebraMap A B (lift R A B x) = algebraMap S B x :=
  algebraMap_mk' A (algebraMap S B x) (IsIntegral.algebraMap (Algebra.IsIntegral.isIntegral (R := R) x))

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