toIsometry_tensorHom — Mathlib

English

The equality between the isometry of the tensor of maps and the tmul of the individual isometries holds as a fundamental property.

Русский

Справедливость равенства между изометрией тензора и tmul индивидуальных изометрий как основное свойство.

LaTeX

$$$ (f \\otimes_{\\mathcal{M}} g).\\mathrm{toIsometry} = f.\\mathrm{toIsometry} \\;\\mathrm{tmul} \\; g.\\mathrm{toIsometry}. $$$

Lean4

theorem toIsometry_tensorHom {K L M N : QuadraticModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) :
    (f ⊗ₘ g).toIsometry = f.toIsometry.tmul g.toIsometry :=
  rfl

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