refl

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.refl

← MathLib Explorer

English

Identity affine equivalence acts as the identity map on the space.

Русский

Идентичное аффинное эквивалентное отображение действует как тождественный отображение.

LaTeX

$$$\text{refl} = \mathrm{id}$$$

Lean4

/-- Identity map as an `AffineEquiv`. -/
@[refl]
def refl : P₁ ≃ᵃ[k] P₁ where
  toEquiv := Equiv.refl P₁
  linear := LinearEquiv.refl k V₁
  map_vadd' _ _ := rfl

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

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

Разделы

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

Аффилиация

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