Composition of submodule inclusions #
The inclusion maps Submodule.inclusion between nested submodules compose along the composite
inequality (Submodule.inclusion_comp_inclusion), as Set.inclusion_comp_inclusion does for sets.
@[simp]
theorem
Submodule.inclusion_comp_inclusion
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p q r : Submodule R M}
(h : p ≤ q)
(h' : q ≤ r)
:
Composing two inclusions of submodules gives the inclusion along the composite inequality.