theorem add_right_inv {A : Type*} [ring A] : ∀ a : A, a + (-a) = 0 :=
begin
intro a,
rw ← add_left_id (a + (-a)),
rw ← add_left_inv (a + (-a)),
rw ← add_assoc (-(a + (-a))) (a + (-a)),
conv in (a + (-a) + (a + (-a)))
begin
rw ← add_assoc,
rw add_assoc (-a),
rw add_left_inv,
rw add_left_id,
end,
end
theorem add_right_id {A : Type*} [ring A] : ∀ a : A, a + 0 = a :=
begin
intro a,
rw ← add_left_inv,
rw add_assoc,
rw add_right_inv,
rw add_left_id,
end
theorem add_right_cancel {A : Type*} [ring A] {a b : A} (c : A) : c + a = c + b → a = b :=
a + b = b + a
This question is a part of the lean LotM.
Rings are a type of structure that takes the rules of addition and multiplication we are familiar with and abstracts them, so we can reason about them. Rings can be defined in a number of ways. Usually this involves giving a bunch of axiom...
