coe_mk

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The equivalence between toEquiv and equality of affine equivalences is maintained under simp.

Русский

Сохранена связь между toEquiv и равенством аффинных эквив через simp.

LaTeX

$$$e.toEquiv = e'.toEquiv \iff e = e'$$$

Lean4

@[simp]
theorem coe_mk (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (h) : ((⟨e, e', h⟩ : P₁ ≃ᵃ[k] P₂) : P₁ → P₂) = e :=
  rfl

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

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

Разделы

Аффилиация

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