coe_one

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The unit 1 in the endomorphism structure corresponds to the identity affine map.

Русский

Единица в структуре единиц отображений соответствует тождественному аффинному отображению.

LaTeX

$$$1 = \mathrm{refl}_{k} P_1$$$

Lean4

@[simp]
theorem coe_one : ⇑(1 : P₁ ≃ᵃ[k] P₁) = id :=
  rfl

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

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

Разделы

Аффилиация

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