nonempty

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.nonempty

English

The linear part of mk' is f'.

Русский

Линейная часть mk' равна f'.

LaTeX

$$mk' f f' p h .linear = f'$$

Lean4

instance nonempty : Nonempty (P1 →ᵃ[k] P2) :=
  (AddTorsor.nonempty : Nonempty P2).map <| const k P1

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

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

Разделы

Аффилиация

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