English
There is a canonical Div structure on Submodule R A, given by x ∈ I / J iff ∀ y ∈ J, x*y ∈ I.
Русский
Существует каноническая структура деления на Submodule R A: x ∈ I / J тогда и только тогда, когда ∀ y ∈ J, x*y ∈ I.
LaTeX
$$$\mathrm{Div}(\mathrm{Submodule}\; R A) = \{\text{обобщение условия } x\cdot y \in I\}$$$
Lean4
/-- The elements of `I / J` are the `x` such that `x • J ⊆ I`.
In fact, we define `x ∈ I / J` to be `∀ y ∈ J, x * y ∈ I` (see `mem_div_iff_forall_mul_mem`),
which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nicer to use in proofs.
This is the general form of the ideal quotient, traditionally written $I : J$.
-/
instance : Div (Submodule R A) :=
⟨fun I J =>
{ carrier := {x | ∀ y ∈ J, x * y ∈ I}
zero_mem' := fun y _ => by
rw [zero_mul]
apply Submodule.zero_mem
add_mem' := fun ha hb y hy => by
rw [add_mul]
exact Submodule.add_mem _ (ha _ hy) (hb _ hy)
smul_mem' := fun r x hx y hy => by
rw [Algebra.smul_mul_assoc]
exact Submodule.smul_mem _ _ (hx _ hy) }⟩
