English
Proofs that the monoid axioms hold: one corresponds to id, multiplication to comp, associativity, and unit laws.
Русский
Доказательства того, что выполняются аксиомы моноида: единица соответствует id, умножение — comp, ассоциативность и единичные законы.
LaTeX
$$theorem comp_assoc (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) : (f.comp g).comp h = f.comp (g.comp h)$$
Lean4
/-- A linear isometry between two modules restricts to a linear isometry
from any submodule `p` of the domain onto the image of that submodule.
This is a version of `LinearMap.submoduleMap` extended to linear isometries. -/
@[simps!]
def submoduleMap (p : Submodule R M) (e : M →ₗᵢ[R] M₁) : p →ₗᵢ[R] (Submodule.map e p) :=
{ e.toLinearMap.submoduleMap p with norm_map' x := e.norm_map' x }
