Abelian_Group_Induces_Entropic_Structure
Provedabelian-groupsentropic-structureproofwiki
Let G be an abelian group. Let the operation * be defined on G such that x * y = x * y⁻¹. Then (G, *) is an entropic structure.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Abelian_Group_Induces_Entropic_Structure {G : Type _} [CommGroup G] : ∀ a b c d : G, (a * b⁻¹) * (c * d⁻¹) = (a * c) * (b⁻¹ * d⁻¹) := by sorrySource