copy_eq

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.copy_eq

English

If f' is the underlying function of f, then the copy equals the original.

Русский

Если f' является базовой функцией f, копия равна исходному отображению.

LaTeX

$$$f.copy f' h = f$$$

Lean4

theorem copy_eq (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : f.copy f' h = f :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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