1.3. Algebraic properties🔗

Because DH is declared as an abbrev, it is definitionally equal to Mathlib's scalar multiplication a • B. All algebraic properties are inherited directly from the Module F G typeclass API in Mathlib (Mathlib.Algebra.Module.Basic), with no additional proofs needed:

• Commutativity: DH a (DH b P) = DH b (DH a P) from smul_smul + mul_comm (Mathlib)

• Associativity: DH a (DH b B) = DH (a * b) B from mul_smul (Mathlib)

• Zero: DH 0 B = 0 from zero_smul (Mathlib)

• One: DH 1 B = B from one_smul (Mathlib)

• Addition: DH (a + b) B = DH a B + DH b B from add_smul (Mathlib)