Theoremsadd, eq_of_add_add_eq_zero, isRefl, neg, neg_eq, self_eq_zero, smul, sub, add, nonneg, smul, add, isNonneg, isSymm, smul, eq_zero, groupSMul, neg, smul, add, eq, isRefl, neg, polarization, restrict, smul, sub, flip, ker_eq_bot, ne_zero, apply_dualBasis_left, apply_dualBasis_right, apply_toDual_symm_apply, compLeft_injective, comp_symmCompOfNondegenerate_apply, dualBasis_dualBasis, dualBasis_dualBasis_flip, dualBasis_eq_iff, dualBasis_flip_dualBasis, dualBasis_injective, dualBasis_involutive, dualBasis_repr_apply, ext_iff_of_isSymm, ext_of_isSymm, isAdjointPairLeftAdjointOfNondegenerate, isAdjointPair_iff_eq_of_nondegenerate, isAdjointPair_unique_of_nondegenerate, isAlt_neg, isAlt_zero, isNonneg_def, isNonneg_iff, isNonneg_zero, isPosSemidef_def, isPosSemidef_iff, isPosSemidef_zero, isRefl_neg, isRefl_zero, isSymm_def, isSymm_iff, isSymm_iff_basis, isSymm_iff_flip, isSymm_neg, isSymm_zero, nonDegenerateFlip_iff, nondegenerate_congr_iff, nondegenerate_flip_iff, not_nondegenerate_zero, symmCompOfNondegenerate_left_apply, toDual_def | 69 |