instInhabited

Mathlib.Topology.Algebra.Module.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.instInhabited

English

The zero continuous alternating map maps to the zero alternating map.

Русский

Нулевое непрерывное чередующееся отображение отображается в нулевое чередующееся отображение.

LaTeX

$$$\\mathrm{toAlternatingMap}(0) = 0$$$

Lean4

instance : Inhabited (M [⋀^ι]→L[R] N) :=
  ⟨0⟩

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

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

Разделы

Аффилиация

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