English
The map CategoryTheory.Iso.toIsometryEquiv respects transitivity of isomorphisms; i.e., toIsometryEquiv (e ≪≫ f) equals e.toIsometryEquiv.trans f.toIsometryEquiv.
Русский
Переход toIsometryEquiv сохраняет транситивность изоморфизмов: toIsometryEquiv (e ≪≫ f) = e.toIsometryEquiv.trans f.toIsometryEquiv.
LaTeX
$$$\\mathrm{toIsometryEquiv}(e \\overset{\\mathrm{trans}}{\\circ} f) = (\\mathrm{toIsometryEquiv}(e)) \\; \\mathrm{.trans} \\; (\\mathrm{toIsometryEquiv}(f))$$$
Lean4
/-- `TensorProduct.map` for `QuadraticForm.Isometry`s -/
def _root_.QuadraticMap.Isometry.tmul {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
{Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) : (Q₁.tmul Q₃) →qᵢ (Q₂.tmul Q₄)
where
toLinearMap := TensorProduct.map f.toLinearMap g.toLinearMap
map_app' := tmul_tensorMap_apply f g
