hom₂_ofHom₂ — Mathlib

English

The canonical isomorphism sends the bilinear interpretation into the original linear interpretation on a type.

Русский

Единичная биекция переводит билинейную интерпретацию в исходную линейную интерпретацию.

LaTeX

$$$\mathrm{ofHom_2}(\mathrm{Hom_2}(f)) = f$$$

Lean4

@[simp]
theorem hom₂_ofHom₂ {M N P : ModuleCat.{u} R} (f : M →ₗ[R] N →ₗ[R] P) : (ofHom₂ f).hom₂ = f :=
  rfl

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