Proof obligations of Mathlib's Group: ∀ a, a * 1 = a

Stream: new members

[Isak Colboubrani]

I have observed that in Mathlib, the Group structure can be defined with minimal proof obligations using Group.ofLeftAxioms. This approach requires:

• Associativity
• A left inverse: ∀ a, a⁻¹ * a = 1
• A left neutral element: ∀ a, 1 * a = a

On the other hand, the conventional Group class appears to demand:

• Associativity
• A left inverse: ∀ a, a⁻¹ * a = 1 (directly in the Group definition)
• A left neutral element: ∀ a, 1 * a = a (via Monoid's MulOneClass requirement)
• A right neutral element: ∀ a, a * 1 = a (via Monoid's MulOneClass requirement)

Note that the right inverse is not explicitly required in this context: it is deduced in mul_right_inv by utilizing a combination of associativity, left inverse, and left neutral element.

My question is: why is the right neutral element mandated in this scenario, rather than being deduced from the amalgamation of associativity, left inverse, and left neutral element, as in the case of mul_right_inv?

[Ruben Van de Velde]

Note that Group inherits from Monoid, and this is where the one_mul and mul_one fields come from. I believe that in this setting, they actually are not redundant

[Patrick Massot]

Yes, this is the explanation. All those tricks to eliminate "redundant" axioms fail for more general algebraic structures. So when building from poor structures to risk structures we cannot take this road. Nothing prevents us to add those tricks on top, as can be seen from Group.ofLeftAxioms but we noticed this is useless.