'KenomaMixedVolume.inner_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_add_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_add_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_sub_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_sub_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_smul_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_smul_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.normSq_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.normSq_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.normSq_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.normSq_smul' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.project_eq_self_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.project_idempotent' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.inner_project' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.project_self_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.optimizer_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.square_completion' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.optimizer_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.objective_le_condensed' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.value_eq_iff_optimizer' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.unique_maximizer' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.pythagoras' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.pointwise_minus_condensed' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.condensed_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.gap_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.gap_zero_iff_represented' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaMixedVolume.nested_energy_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]