refl_trans — Mathlib

English

Let e be an affine equivalence P1 ≃ᵃ[k] P2. The identity affine equivalence on P1 acts as a left identity for composition: the composition of the identity with e equals e.

Русский

Пусть e — аффинное эквивалентное отображение P1 ≃ᵃ[k] P2. Тождественное аффинное отображение на P1 слева по отношению к композиции является нейтральным элементом: идентность слева от e дает e.

LaTeX

$$$(\mathrm{refl}\;k\;P_1) \;\text{is the left identity for affine composition:} \; (\mathrm{refl}\;k\;P_1) \;\trans\; e = e.$$$

Lean4

@[simp]
theorem refl_trans (e : P₁ ≃ᵃ[k] P₂) : (refl k P₁).trans e = e :=
  ext fun _ => rfl

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