1.2. Notation🔗

The formalization uses additive group notation following the Mathlib convention, instead of the multiplicative notation from textbooks:

• gᵃ becomes a • G₀ (scalar multiplication)

• (gᵃ)ᵇ = gᵃᵇ becomes b • (a • G₀) = (b * a) • G₀

• gᵃ · gᵇ = gᵃ⁺ᵇ becomes a • G₀ + b • G₀ = (a + b) • G₀