group.one?

Stream: general

[Kenny Lau]

This is the definition of group:

class group (α : Type u) extends monoid α, has_inv α :=
(mul_left_inv : ∀ a : α, a⁻¹ * a = 1)

then how does this produce group.one?

[Reid Barton]

Probably monoid extends has_one?

[Simon Hudon]

Yes it does and group is an old_structure