coe_liftLie_eq_lift_coe

Mathlib.Algebra.Lie.TensorProduct

URI: https://scilib.ai/kg/mathlib#TensorProduct.LieModule.coe_liftLie_eq_lift_coe

English

The underlying function of liftLie applied to f equals the lift of f: coe(liftLie f) = lift f.

Русский

Пределяемая функция подъема applied к f равна lift f: coe(liftLie f) = lift f.

LaTeX

$$$\operatorname{coe}\big(\mathrm{liftLie}\,R\,L\,M\,N\,P\,f\big) = \mathrm{lift}\,R\,L\,M\,N\,P\,f$$$

Lean4

@[simp]
theorem coe_liftLie_eq_lift_coe (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) : ⇑(liftLie R L M N P f) = lift R L M N P f := by tauto

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

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

Разделы

Аффилиация

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