toAffineSubspace_direction

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.toAffineSubspace_direction

← MathLib Explorer

English

The direction of s.toAffineSubspace equals s for a submodule s.

Русский

Направление s.toAffineSubspace равно s для подмодуля s.

LaTeX

$$$s.toAffineSubspace.direction = s$$$

Lean4

@[simp]
theorem toAffineSubspace_direction (s : Submodule k V) : s.toAffineSubspace.direction = s := by ext x;
  simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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