Chris Hughes (Aug 24 2019 at 15:55):
If I import
#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