Zulip Chat Archive

Stream: general

Topic: wrong associativity in docs


Junyan Xu (May 07 2022 at 19:44):

docs#semigroup shows
mul_assoc : ∀ (a b c : G), (a * b) * c = a * b * c
but in the source it's
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
so it seems doc_gen somehow assumes * is right-associative?

Reid Barton (May 07 2022 at 19:48):

most likely related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pow.2Fmul.20associativity/near/264683881


Last updated: Dec 20 2023 at 11:08 UTC