quotient_group._to_additive axiom

Stream: maths

[Chris Hughes]

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.