funCongrLeft_id — Mathlib

English

The congrLeft construction with the identity equivalence equals the identity linear equivalence on the function space: funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M).

Русский

Конглев слева от тождества совпадает с тождественным линейным эквивелентом на пространстве функций: funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M).

LaTeX

$$$ \mathrm{funCongrLeft}(R,M,\mathrm{Equiv.refl}\, n) = \mathrm{LinearEquiv.refl}\, R\,(n\to M) $$$

Lean4

@[simp]
theorem funCongrLeft_id : funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M) :=
  rfl

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