coe_toAffineEquiv — Mathlib

English

The underlying function of the affine version of a linear equivalence is the same as the linear equivalence itself.

Русский

Базовая функция аффинного варианта линейного эквивалентного отображения совпадает с самим линейным эквивалентом.

LaTeX

$$coe_toAffineEquiv(e) : (e.toAffineEquiv) = e$$

Lean4

@[simp]
theorem coe_toAffineEquiv (e : V₁ ≃ₗ[k] V₂) : ⇑e.toAffineEquiv = e :=
  rfl

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