Trivial_Ring_from_Abelian_Group
Provedabelian-groupsproofwikirings
Any abelian group (G, +) may be turned into a trivial ring by defining the ring product to be x * y = 0 for all x, y in G.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Trivial_Ring_from_Abelian_Group {G : Type _} [AddCommGroup G] : ∃ (mul : G → G → G), (∀ x y : G, mul x y = 0) ∧ (∀ a b c : G, mul a (b + c) = mul a b + mul a c) := by sorrySource