setLike — Mathlib

English

There is a SetLike instance for HomogeneousSubmodule with the underlying carrier as its Submodule.

Русский

Существует экземпляр SetLike для HomogeneousSubmodule, у которого базовый носитель — это Submodule.

LaTeX

$$$$ \text{SetLike} (\text{HomogeneousSubmodule } 𝒜 \ℳ) M. $$$$

Lean4

instance setLike : SetLike (HomogeneousSubmodule 𝒜 ℳ) M
    where
  coe p := p.toSubmodule
  coe_injective' _ _ h := HomogeneousSubmodule.toSubmodule_injective 𝒜 ℳ <| SetLike.coe_injective h

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