ext

Mathlib.Algebra.Module.LinearMap.Defs

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

English

Two semilinear maps are equal if they agree on every input.

Русский

Два полулинейных отображения равны, если они совпадают на всех входах.

LaTeX

$$$\forall x,\; f(x) = g(x) \Rightarrow f = g$$$

Lean4

@[ext]
theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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

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

Разделы

Аффилиация

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