| Name | Category | Theorems |
|---|
Antivary 📖 | MathDef | 85 mathmath: Antivary.mul_left, Antivary.nsmul_right, Antivary.of_inv₀, Monotone.antivary, Antivary.div_right, monovary_inv_left, Antivary.sub_left, antivary_iff_smul_rearrangement, antivary_inv₀, Monovary.dual_left, Antitone.antivary, Antivary.neg, antivary_inv, Monovary.of_inv_left, monovary_toDual_right, monovary_inv_right₀, Monovary.of_neg_left, antivary_inv_right₀, Monovary.inv_right, antivaryOn_univ, Antivary.mul_right₀, Antivary.sum_smul_lt_sum_comp_perm_smul_iff, Monovary.neg_right, antivary_neg, Monovary.inv_left, antivary_toDual_right, antivary_iff_exists_monotone_antitone, Antivary.sum_mul_eq_sum_mul_comp_perm_iff, Antivary.add_right, Antivary.inv, Monovary.inv_right₀, Antivary.inv₀, Antivary.pow_left, Antivary.add_left, Antivary.sum_smul_lt_sum_smul_comp_perm_iff, Monovary.inv_left₀, antivary_inv_left, Monovary.dual_right, antivaryOn_iff_antivary, Antivary.pow_right₀, antivary_neg_left, Antivary.mul_left₀, Antivary.mul_right, antivary_iff_mul_rearrangement, antivary_id_iff, Antivary.comp_right, Antivary.sub_right, Antivary.of_neg, Antivary.sum_mul_lt_sum_comp_perm_mul_iff, antivary_const_right, monovary_toDual_left, Monovary.of_inv_right, Antivary.div_right₀, Antivary.sum_smul_comp_perm_eq_sum_smul_iff, Monovary.comp_antitone_left, antivary_toDual_left, antivary_iff_forall_mul_nonpos, Antivary.nsmul_left, Subsingleton.antivary, Monovary.of_inv_right₀, monovary_inv_left₀, antivary_iff_forall_smul_nonpos, Antivary.div_left₀, Antivary.pow_left₀, antivary_comm, monovary_neg_right, Antivary.comp_monotone_left, monovary_inv_right, antivary_const_left, Antivary.sum_comp_perm_mul_eq_sum_mul_iff, Antivary.symm, Monovary.of_inv_left₀, Monovary.of_neg_right, Antivary.sum_mul_lt_sum_mul_comp_perm_iff, Antivary.div_left, antivary_neg_right, antivary_inv_left₀, monovary_neg_left, Antivary.pow_right, Antivary.of_inv, Antivary.dual, antivary_iff_exists_antitone_monotone, antivary_inv_right, Monovary.neg_left, Antivary.sum_comp_perm_smul_eq_sum_smul_iff
|
AntivaryOn 📖 | MathDef | 90 mathmath: AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff, AntivaryOn.subset, AntivaryOn.dual, AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff, antivaryOn_comm, AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff, AntivaryOn.div_right₀, MonovaryOn.inv_right, AntivaryOn.mul_left, MonovaryOn.of_inv_right, antivaryOn_toDual_left, antivaryOn_inv_left₀, antivaryOn_inv_right, AntitoneOn.antivaryOn, MonovaryOn.dual_left, antivaryOn_const_left, monovaryOn_inv_right, MonovaryOn.of_neg_left, MonovaryOn.of_inv_left, antivaryOn_neg_left, MonovaryOn.inv_left₀, antivaryOn_univ, AntivaryOn.of_neg, MonovaryOn.inv_right₀, AntivaryOn.div_right, MonovaryOn.dual_right, antivaryOn_iff_exists_monotoneOn_antitoneOn, monovaryOn_toDual_right, AntivaryOn.add_left, AntivaryOn.mul_left₀, monovaryOn_neg_right, AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff, antivaryOn_inv₀, AntivaryOn.of_inv, AntivaryOn.mul_right₀, AntivaryOn.nsmul_left, AntivaryOn.div_left₀, AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff, MonovaryOn.of_inv_left₀, AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff, MonovaryOn.comp_antitoneOn_right, monovaryOn_neg_left, antivaryOn_inv, MonotoneOn.antivaryOn, AntivaryOn.pow_left₀, AntivaryOn.sub_right, antivaryOn_iff_antivary, AntivaryOn.empty, antivaryOn_inv_left, AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff, antivaryOn_iff_smul_rearrangement, AntivaryOn.comp_right, MonovaryOn.of_inv_right₀, AntivaryOn.pow_right₀, antivaryOn_neg, monovaryOn_inv_left₀, AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff, antivaryOn_id_iff, antivaryOn_iff_forall_mul_nonpos, AntivaryOn.inv, antivaryOn_toDual_right, AntivaryOn.of_inv₀, MonovaryOn.neg_right, AntivaryOn.div_left, antivaryOn_neg_right, AntivaryOn.comp_monotoneOn_right, AntivaryOn.mul_right, antivaryOn_iff_exists_antitoneOn_monotoneOn, antivaryOn_const_right, AntivaryOn.sub_left, antivaryOn_iff_forall_smul_nonpos, AntivaryOn.neg, antivaryOn_iff_mul_rearrangement, AntivaryOn.inv₀, MonovaryOn.inv_left, MonovaryOn.of_neg_right, antivaryOn_inv_right₀, MonovaryOn.comp_antitone_on_left, AntivaryOn.pow_left, AntivaryOn.symm, AntivaryOn.add_right, MonovaryOn.neg_left, AntivaryOn.nsmul_right, monovaryOn_toDual_left, monovaryOn_inv_right₀, Antivary.antivaryOn, AntivaryOn.comp_monotone_on_left, AntivaryOn.pow_right, monovaryOn_inv_left, Subsingleton.antivaryOn
|
Monovary 📖 | MathDef | 86 mathmath: Monovary.sum_mul_comp_perm_eq_sum_mul_iff, Antivary.inv_right, monovary_inv, monovary_iff_mul_rearrangement, monovary_inv_left, Antivary.neg_right, Antivary.of_neg_right, Monovary.of_inv, monovary_toDual_right, Monovary.pow_right₀, Monovary.div_right₀, monovary_inv_right₀, Antivary.inv_right₀, monovaryOn_iff_monovary, Monovary.pow_left₀, Antivary.neg_left, Antivary.dual_left, Monovary.sub_right, Antivary.inv_left₀, Monovary.mul_right₀, antivary_inv_right₀, monovary_iff_forall_smul_nonneg, monovary_neg, antivary_toDual_right, monovary_iff_smul_rearrangement, Monovary.sum_comp_perm_smul_lt_sum_smul_iff, monovary_comm, monovary_iff_exists_antitone, Monovary.div_right, Monovary.mul_right, Antivary.of_inv_left₀, monovary_self, Monovary.comp_monotone_left, antivary_inv_left, Antivary.of_inv_left, Monotone.monovary, Monovary.mul_left, Monovary.inv₀, antivary_neg_left, monovary_id_iff, Monovary.sum_comp_perm_mul_eq_sum_mul_iff, monovary_const_left, monovary_const_right, monovaryOn_univ, Monovary.sum_smul_comp_perm_lt_sum_smul_iff, Monovary.nsmul_left, Monovary.sum_comp_perm_mul_lt_sum_mul_iff, monovary_iff_forall_mul_nonneg, Monovary.comp_right, Monovary.inv, Monovary.div_left₀, Monovary.sum_comp_perm_smul_eq_sum_smul_iff, Monovary.add_left, Monovary.of_inv₀, Monovary.add_right, monovary_toDual_left, Monovary.div_left, Monovary.pow_right, Monovary.sum_mul_comp_perm_lt_sum_mul_iff, Monovary.symm, monovary_inv₀, Antivary.of_inv_right, antivary_toDual_left, Antivary.dual_right, Antitone.monovary, Monovary.dual, monovary_inv_left₀, Monovary.pow_left, monovary_neg_right, monovary_inv_right, Monovary.nsmul_right, Monovary.of_neg, Monovary.mul_left₀, Monovary.sub_left, Subsingleton.monovary, antivary_neg_right, Antivary.inv_left, antivary_inv_left₀, monovary_neg_left, antivary_inv_right, Antivary.comp_antitone_left, Antivary.of_inv_right₀, monovary_iff_exists_monotone, Monovary.neg, Monovary.sum_smul_comp_perm_eq_sum_smul_iff, Antivary.of_neg_left
|
MonovaryOn 📖 | MathDef | 91 mathmath: AntivaryOn.comp_antitoneOn_right, AntivaryOn.of_inv_right₀, monovaryOn_inv₀, MonovaryOn.nsmul_left, MonovaryOn.mul_right, Monovary.monovaryOn, MonovaryOn.mul_right₀, AntivaryOn.neg_left, MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff, AntivaryOn.inv_left₀, MonovaryOn.pow_right, MonovaryOn.subset, MonovaryOn.symm, antivaryOn_toDual_left, monovaryOn_inv, antivaryOn_inv_left₀, MonovaryOn.div_right₀, AntitoneOn.monovaryOn, AntivaryOn.dual_right, monovaryOn_comm, antivaryOn_inv_right, monovaryOn_neg, monovaryOn_const_right, MonovaryOn.mul_left₀, monovaryOn_iff_forall_smul_nonneg, monovaryOn_iff_monovary, monovaryOn_inv_right, MonovaryOn.pow_right₀, monovaryOn_self, antivaryOn_neg_left, MonovaryOn.add_right, MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff, MonovaryOn.of_inv, MonovaryOn.empty, MonovaryOn.pow_left, AntivaryOn.of_neg_right, monovaryOn_iff_exists_monotoneOn, monovaryOn_toDual_right, monovaryOn_neg_right, MonovaryOn.of_neg, AntivaryOn.comp_antitone_on_left, MonovaryOn.neg, monovaryOn_iff_smul_rearrangement, monovaryOn_neg_left, MonovaryOn.div_right, antivaryOn_inv_left, MonovaryOn.div_left₀, MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff, MonovaryOn.of_inv₀, MonovaryOn.comp_monotone_on_left, monovaryOn_univ, MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff, MonovaryOn.inv₀, AntivaryOn.of_inv_left₀, MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff, monovaryOn_inv_left₀, MonovaryOn.nsmul_right, Subsingleton.monovaryOn, MonovaryOn.comp_right, monovaryOn_id_iff, AntivaryOn.dual_left, MonotoneOn.monovaryOn, antivaryOn_toDual_right, MonovaryOn.sub_right, MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff, AntivaryOn.inv_right₀, AntivaryOn.neg_right, AntivaryOn.of_neg_left, antivaryOn_neg_right, MonovaryOn.pow_left₀, monovaryOn_const_left, MonovaryOn.inv, MonovaryOn.add_left, MonovaryOn.div_left, monovaryOn_iff_exists_antitoneOn, monovaryOn_iff_mul_rearrangement, AntivaryOn.of_inv_left, MonovaryOn.comp_monotoneOn_right, AntivaryOn.inv_right, AntivaryOn.inv_left, antivaryOn_inv_right₀, MonovaryOn.dual, MonovaryOn.mul_left, AntivaryOn.of_inv_right, monovaryOn_toDual_left, monovaryOn_inv_right₀, MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff, MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff, MonovaryOn.sub_left, monovaryOn_inv_left, monovaryOn_iff_forall_mul_nonneg
|