'trace_spiral' depends on axioms: [propext, Classical.choice, Quot.sound]
'det_spiral' depends on axioms: [propext, Classical.choice, Quot.sound]
'discriminant' depends on axioms: [propext, Classical.choice, Quot.sound]
'is_spiral' depends on axioms: [propext, Classical.choice, Quot.sound]
'is_sink_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'trace_of_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'det_of_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'similar_forces_same_invariants' depends on axioms: [propext, Classical.choice, Quot.sound]
'different_mu_not_similar' depends on axioms: [propext, Classical.choice, Quot.sound]
'immune_is_not_market' depends on axioms: [propext, Classical.choice, Quot.sound]