English
For submodules N, P of a module M over R, define N : P = { r ∈ R | r·P ⊆ N }.
Русский
Для подмодулей N, P модуля M над R задаём N : P = { r ∈ R | r·P ⊆ N }.
LaTeX
$$\\operatorname{colon}(N,P) = \\{ r ∈ R \\mid r·P \\subseteq N \\}$$
Lean4
/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`. -/
def colon (N P : Submodule R M) : Ideal R
where
carrier := {r : R | (r • P : Set M) ⊆ N}
add_mem' ha hb := (Set.add_smul_subset _ _ _).trans ((Set.add_subset_add ha hb).trans_eq (by simp))
zero_mem' := by simp [Set.zero_smul_set P.nonempty]
smul_mem'
r := by
simp only [Set.mem_setOf_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]
intro x hx y hy
exact N.smul_mem _ (hx hy)
