leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: group.one?


Kenny Lau (Sep 02 2018 at 06:10):

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 (Sep 02 2018 at 07:04):

Probably monoid extends has_one?

Simon Hudon (Sep 02 2018 at 07:04):

Yes it does and group is an old_structure


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll