Zulip Chat Archive

Stream: maths

Topic: quotient_group._to_additive axiom


view this post on Zulip Chris Hughes (Aug 24 2019 at 15:55):

If I import group_theory.coset and #print axioms it shows quotient_group._to_additive : Type This is because on line 141 there is a run_cmd that as far as I can tell adds this axiom and nothing else. I'm guessing this isn't the intended behaviour. Maybe something was unfinished.


Last updated: May 19 2021 at 02:10 UTC