refl_apply — Mathlib

English

The coercion of the identity affine equivalence to an affine map is the identity affine map.

Русский

Приведение тождественного аффинного эквивалента к аффинному отображению даёт тождественное аффинное отображение.

LaTeX

$$$\mathrm{coe\;refl\;to\;affineMap}:\; \mathrm{refl}\;\to\; \mathrm{AffineMap.id}$.$$

Lean4

@[simp]
theorem refl_apply (x : P₁) : refl k P₁ x = x :=
  rfl

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