English
There exists a two-sided ideal constructed from a carrier with specified closure properties.
Русский
Существует двусторонний идеал, построенный из множества-носителя с указанными свойствами замыкания.
LaTeX
$$mk'(carrier, zero_mem, add_mem, neg_mem, mul_mem_left, mul_mem_right) : TwoSidedIdeal R$$
Lean4
/-- The "set-theoretic-way" of constructing a two-sided ideal by providing:
- the underlying set `S`;
- a proof that `0 ∈ S`;
- a proof that `x + y ∈ S` if `x ∈ S` and `y ∈ S`;
- a proof that `-x ∈ S` if `x ∈ S`;
- a proof that `x * y ∈ S` if `y ∈ S`;
- a proof that `x * y ∈ S` if `x ∈ S`.
-/
def mk' (carrier : Set R) (zero_mem : 0 ∈ carrier) (add_mem : ∀ {x y}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
(neg_mem : ∀ {x}, x ∈ carrier → -x ∈ carrier) (mul_mem_left : ∀ {x y}, y ∈ carrier → x * y ∈ carrier)
(mul_mem_right : ∀ {x y}, x ∈ carrier → x * y ∈ carrier) : TwoSidedIdeal R where
ringCon :=
{ r := fun x y ↦ x - y ∈ carrier
iseqv :=
{ refl := fun x ↦ by simpa using zero_mem
symm := fun h ↦ by simpa using neg_mem h
trans := fun {x y z} h1 h2 ↦ by simpa only [show x - z = (x - y) + (y - z) by abel] using add_mem h1 h2 }
mul' := fun {a b c d} (h1 : a - b ∈ carrier) (h2 : c - d ∈ carrier) ↦
show _ ∈ carrier
by
rw [show a * c - b * d = a * (c - d) + (a - b) * d by rw [mul_sub, sub_mul]; abel]
exact add_mem (mul_mem_left h2) (mul_mem_right h1)
add' := fun {a b c d} (h1 : a - b ∈ carrier) (h2 : c - d ∈ carrier) ↦
show _ ∈ carrier by
rw [show a + c - (b + d) = (a - b) + (c - d) by abel]
exact add_mem h1 h2 }
