lift_eq

Mathlib.RingTheory.IsTensorProduct

URI: https://scilib.ai/kg/mathlib#IsTensorProduct.lift_eq

English

For any f' and x1,x2, h.lift f' (f x1 x2) = f' x1 x2.

Русский

Для любого f' и элементов x1,x2 выполняется h.lift f' (f x1 x2) = f' x1 x2.

LaTeX

$$h.lift f' (f x1 x2) = f' x1 x2$$

Lean4

theorem lift_eq (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁) (x₂ : M₂) :
    h.lift f' (f x₁ x₂) = f' x₁ x₂ := by simp [lift]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru