toEquiv_refl

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The underlying equivalence of the identity affine equivalence is the identity equivalence.

Русский

Базовая эквивалентность тождественного аффинного эквивалента равна тождественной эквивалентности.

LaTeX

$$$\mathrm{toEquiv}(\mathrm{refl}) = \mathrm{Equiv.refl}$$$

Lean4

@[simp]
theorem toEquiv_refl : (refl k P₁).toEquiv = Equiv.refl P₁ :=
  rfl

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

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

Разделы

Аффилиация

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