English
Naturality of the inner quotient equivalence with respect to a linear map f; two composed maps agree.
Русский
Естественность внутреннего эквивалентного отображения относительно линейного отображения f; две композиции совпадают.
LaTeX
$$$((\\text{QuotOfListConsSMulTopEquivQuotSMulTopInner M_2 r rs).toLinearMap) \\circ (mapQ\\; _\\; _\\; (smul_top_le_comap_smul_top (\\text{Ideal.ofList } (r :: rs)) f)) = (mapQ\\; _\\; _\\; (smul_top_le_comap_smul_top _ (\\text{QuotSMulTop.map } r f))) \\circ ((\\text{QuotOfListConsSMulTopEquivQuotSMulTopInner M r rs}).toLinearMap)$$$
Lean4
theorem smul_top_le_comap_smul_top [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
(I : Ideal R) (f : M →ₗ[R] M₂) : I • ⊤ ≤ comap f (I • ⊤) :=
map_le_iff_le_comap.mp <| le_of_eq_of_le (map_smul'' _ _ _) <| smul_mono_right _ le_top
