lift_tmul — Mathlib

English

If two lifts coincide, their equality propagates through the construction: if f, f_1 and g, g_1 are equal and hfg, e_f, e_g express the same commuting data, then lift f g hfg = lift f_1 g_1 hfg_1.

Русский

Если две конструкции лифта совпадают, то их равенство сохраняется: если f = f_1, g = g_1 и hfg равносильно совпадающим данным, то lift f g hfg = lift f_1 g_1 hfg_1.

LaTeX

$$$\\text{Eq }(\\mathrm{lift}\; f\; g\; hfg)\; (\\mathrm{lift}\\; f_1\\; g_1\\; hfg_1) , \\text{ given } e_f: f=f_1, e_g: g=g_1, \\text{ and } hfg= hfg_1.$$$

Lean4

@[simp]
theorem lift_tmul (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) (a : A) (b : B) :
    lift f g hfg (a ⊗ₜ b) = f a * g b :=
  rfl

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