Last active
January 18, 2023 19:42
-
-
Save jcommelin/1299f6a0b10e823c96bb251902f209ef to your computer and use it in GitHub Desktop.
to_additive #align failures
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ❌ le_of_forall_neg_add_le <- ✅ le_of_forall_lt_one_mul_le | |
| ❌ le_iff_forall_neg_add_le <- ✅ le_iff_forall_lt_one_mul_le | |
| ❌ Sum.FaithfulVAddLeft <- ✅ Sum.FaithfulSMulLeft | |
| ❌ nsmul_le_nsmul_iff <- ✅ pow_le_pow_iff' | |
| ❌ Multiset.sum_zero <- ✅ Multiset.prod_zero | |
| ❌ nsmul_lt_nsmul_iff <- ✅ pow_lt_pow_iff' | |
| ❌ Part.left_dom_of_sub_dom <- ✅ Part.left_dom_of_div_dom | |
| ❌ Pi.update_eq_sub_add_single <- ✅ Pi.update_eq_div_mul_mulSingle | |
| ❌ eq_zero_or_pos <- ✅ eq_one_or_one_lt | |
| ❌ WithBot.coe_eq_zero <- ✅ WithBot.coe_eq_one | |
| ❌ Set.Nonempty.neg <- ✅ Set.Nonempty.inv | |
| ❌ Set.empty_nsmul <- ✅ Set.empty_pow | |
| ❌ Option.vadd_some <- ✅ Option.smul_some | |
| ❌ AddSubmonoid.centralizer_to_add_subsemigroup <- ✅ Submonoid.centralizer_toSubsemigroup | |
| ❌ AddSubsemigroup.mem_supₛ_of_mem <- ✅ Subsemigroup.mem_supₛ_of_mem | |
| ❌ AddCommSemigroup.IsRightCancelAdd.toIsCancelAdd <- ✅ CommSemigroup.IsRightCancelMul.toIsCancelMul | |
| ❌ Pi.existsAddOfLe <- ✅ Pi.existsMulOfLe | |
| ❌ neg_lt <- ✅ inv_lt' | |
| ❌ add_neg_le_iff_le_add <- ✅ mul_inv_le_iff_le_mul | |
| ❌ AddSubmonoid.dense_induction <- ✅ Submonoid.dense_induction | |
| ❌ Set.mem_vadd <- ✅ Set.mem_smul | |
| ❌ FreeAddMonoid.lift <- ✅ FreeMonoid.lift | |
| ❌ AddUnits.min_val <- ✅ Units.min_val | |
| ❌ AddSubmonoid.not_mem_of_not_mem_closure <- ✅ Submonoid.not_mem_of_not_mem_closure | |
| ❌ FreeAddMonoid.toList_sum <- ✅ FreeMonoid.toList_prod | |
| ❌ OneHomClass.map_one -> ✅ ZeroHomClass.map_zero | |
| ❌ Function.const_nonneg_of_nonneg <- ✅ Function.one_le_const_of_one_le | |
| ❌ Multiset.sum_replicate <- ✅ Multiset.prod_replicate | |
| ❌ List.headI_add_tail_sum_of_ne_nil <- ✅ List.headI_mul_tail_prod_of_ne_nil | |
| ❌ AddCancelMonoid.toAddLeftCancelMonoid_injective <- ✅ CancelMonoid.toLeftCancelMonoid_injective | |
| ❌ List.sum_isAddUnit_iff <- ✅ List.prod_isUnit_iff | |
| ❌ FreeAddMonoid.ofList_vadd <- ✅ FreeMonoid.ofList_smul | |
| ❌ AddMonoidHom.eqOn_closureM <- ✅ MonoidHom.eqOn_closureM | |
| ❌ IsAddHom.add <- ✅ IsMulHom.mul | |
| ❌ Multiset.sum_induction <- ✅ Multiset.prod_induction | |
| ❌ List.get?_zero_add_tail_sum <- ✅ List.get?_zero_mul_tail_prod | |
| ❌ AddRightCancelMonoid.ext <- ✅ RightCancelMonoid.ext | |
| ❌ Set.unionᵢ_op_vadd_set <- ✅ Set.unionᵢ_op_smul_set | |
| ❌ Right.nonneg_neg_iff <- ✅ Right.one_le_inv_iff | |
| ❌ List.sum_take_add_sum_drop <- ✅ List.prod_take_mul_prod_drop | |
| ❌ AddCancelCommMonoid.toAddCommMonoid_injective <- ✅ CancelCommMonoid.toCommMonoid_injective | |
| ❌ Set.inter_add_subset <- ✅ Set.inter_mul_subset | |
| ❌ AddMonoidHom.map_mul₂ <- ✅ MonoidHom.map_mul₂ | |
| ❌ Set.singleton_vadd_singleton <- ✅ Set.singleton_smul_singleton | |
| ❌ IsAddGroupHom.injective_iff <- ✅ IsGroupHom.injective_iff | |
| ❌ Set.vadd_set_interᵢ_subset <- ✅ Set.smul_set_interᵢ_subset | |
| ❌ Set.unionᵢ₂_sub <- ✅ Set.unionᵢ₂_div | |
| ❌ min_add_add_left <- ✅ min_mul_mul_left | |
| ❌ nsmul_pos <- ✅ one_lt_pow' | |
| ❌ Sum.vadd_inl <- ✅ Sum.smul_inl | |
| ❌ Set.sub_interᵢ₂_subset <- ✅ Set.div_interᵢ₂_subset | |
| ❌ Set.interᵢ₂_add_subset <- ✅ Set.interᵢ₂_mul_subset | |
| ❌ AddSubsemigroup.supᵢ_induction <- ✅ Subsemigroup.supᵢ_induction | |
| ❌ LatticeOrderedCommGroup.abs_sub_sup_add_abs_sub_inf <- ✅ LatticeOrderedCommGroup.abs_div_sup_mul_abs_div_inf | |
| ❌ lt_neg_add_iff_lt <- ✅ lt_inv_mul_iff_lt | |
| ❌ IsAddGroupHom.mk' <- ✅ IsGroupHom.mk' | |
| ❌ Part.zero_mem_zero <- ✅ Part.one_mem_one | |
| ❌ Set.image_vadd <- ✅ Set.image_smul | |
| ❌ Set.interᵢ₂_vadd_subset <- ✅ Set.interᵢ₂_smul_subset | |
| ❌ WithBot.coe_lt_zero <- ✅ WithBot.coe_lt_one | |
| ❌ Right.neg_pos_iff <- ✅ Right.one_lt_inv_iff | |
| ❌ Set.preimage_sub_preimage_subset <- ✅ Set.preimage_div_preimage_subset | |
| ❌ Right.pow_nonneg <- ✅ Right.one_le_pow_of_le | |
| ❌ List.sum_lt_sum_of_ne_nil <- ✅ List.prod_lt_prod_of_ne_nil | |
| ❌ Set.nsmul_mem_nsmul <- ✅ Set.pow_mem_pow | |
| ❌ Set.union_add <- ✅ Set.union_mul | |
| ❌ FreeAddMonoid <- ✅ FreeMonoid | |
| ❌ LatticeOrderedCommGroup.abs_neg_comm <- ✅ LatticeOrderedCommGroup.abs_inv_comm | |
| ❌ AddSubmonoid.closure_singleton_le_iff_mem <- ✅ Submonoid.closure_singleton_le_iff_mem | |
| ❌ Set.add_univ <- ✅ Set.mul_univ | |
| ❌ Left.neg_le_self <- ✅ Left.inv_le_self | |
| ❌ FreeAddMonoid.lift_restrict <- ✅ FreeMonoid.lift_restrict | |
| ❌ le_neg_add_iff_add_le <- ✅ le_inv_mul_iff_mul_le | |
| ❌ Set.vadd_inter_ne_empty_iff <- ✅ Set.smul_inter_ne_empty_iff | |
| ❌ exists_pos_add_of_lt <- ✅ exists_one_lt_mul_of_lt | |
| ❌ sub_lt_iff_lt_add' <- ✅ div_lt_iff_lt_mul' | |
| ❌ Multiset.sum_eq_smul_single <- ✅ Multiset.prod_eq_pow_single | |
| ❌ VAdd.comp.vaddCommClass' <- ✅ SMul.comp.smulCommClass' | |
| ❌ exists_pos_add_of_lt' <- ✅ exists_one_lt_mul_of_lt' | |
| ❌ AddSubmonoid.mem_closure <- ✅ Submonoid.mem_closure | |
| ❌ AddAction.Supports.mono <- ✅ MulAction.Supports.mono | |
| ❌ le_sub_self_iff <- ✅ le_div_self_iff | |
| ❌ Function.const_nonneg <- ✅ Function.one_le_const | |
| ❌ AddAction.Supports.vadd <- ✅ MulAction.Supports.smul | |
| ❌ neg_vadd_eq_iff <- ✅ inv_smul_eq_iff | |
| ❌ VAdd.comp <- ✅ SMul.comp | |
| ❌ sub_lt_self_iff <- ✅ div_lt_self_iff | |
| ❌ AddCon.le_iff <- ✅ Con.le_iff | |
| ❌ Set.add_eq_empty <- ✅ Set.mul_eq_empty | |
| ❌ add_neg_le_iff_le_add' <- ✅ mul_inv_le_iff_le_mul' | |
| ❌ vadd_left_injective' <- ✅ smul_left_injective' | |
| ❌ AddSubmonoid.coe_inf <- ✅ Submonoid.coe_inf | |
| ❌ AddMonoidHom.flipHom <- ✅ MonoidHom.flipHom | |
| ❌ Set.vadd_set_inter <- ✅ Set.smul_set_inter | |
| ❌ AddSubmonoid.mem_top <- ✅ Submonoid.mem_top | |
| ❌ AddMonoidHom.map_div₂ <- ✅ MonoidHom.map_div₂ | |
| ❌ Multiset.sum_nonneg <- ✅ Multiset.one_le_prod_of_one_le | |
| ❌ AddCon.quotientKerEquivOfSurjective <- ✅ Con.quotientKerEquivOfSurjective | |
| ❌ List.sum_append <- ✅ List.prod_append | |
| ❌ Multiset.sum_bind <- ✅ Multiset.prod_bind | |
| ❌ Set.unionᵢ_vadd_right_image <- ✅ Set.unionᵢ_smul_right_image | |
| ❌ Part.neg_mem_neg <- ✅ Part.inv_mem_inv | |
| ❌ Set.vaddCommClass <- ✅ Set.smulCommClass | |
| ❌ VAddAssocClass.opposite_mid <- ✅ IsScalarTower.opposite_mid | |
| ❌ AddMonoidHom.map_list_sum <- ✅ MonoidHom.map_list_prod | |
| ❌ Set.compl_neg <- ✅ Set.compl_inv | |
| ❌ AddSemigroup.to_isAssociative <- ✅ Semigroup.to_isAssociative | |
| ❌ Set.Nonempty.sub <- ✅ Set.Nonempty.div | |
| ❌ AddCon.lift_surjective_of_surjective <- ✅ Con.lift_surjective_of_surjective | |
| ❌ Set.interᵢ_vadd_subset <- ✅ Set.interᵢ_smul_subset | |
| ❌ AddCon.ker_rel <- ✅ Con.ker_rel | |
| ❌ Set.add_inter_subset <- ✅ Set.mul_inter_subset | |
| ❌ List.sum_eq_card_nsmul <- ✅ List.prod_eq_pow_card | |
| ❌ LinearOrderedAddCommGroup.add_lt_add_left <- ✅ LinearOrderedCommGroup.mul_lt_mul_left' | |
| ❌ AddSubmonoid.add_mem <- ✅ Submonoid.mul_mem | |
| ❌ Multiset.sum_map_smul <- ✅ Multiset.prod_map_pow | |
| ❌ Neg.toHasAbs <- ✅ Inv.toHasAbs | |
| ❌ AddHom.restrict <- ✅ MulHom.restrict | |
| ❌ EckmannHilton.addCommMonoid <- ✅ EckmannHilton.commMonoid | |
| ❌ List.exists_lt_of_sum_lt <- ✅ List.exists_lt_of_prod_lt' | |
| ❌ FreeAddMonoid.ofList_append <- ✅ FreeMonoid.ofList_append | |
| ❌ vadd_assoc <- ✅ smul_assoc | |
| ❌ LatticeOrderedCommGroup.abs_of_nonneg <- ✅ LatticeOrderedCommGroup.mabs_of_one_le | |
| ❌ AddSubmonoid.copy <- ✅ Submonoid.copy | |
| ❌ le_neg_iff_add_nonpos_left <- ✅ le_inv_iff_mul_le_one_left | |
| ❌ AddCon.sub <- ✅ Con.div | |
| ❌ nsmul_nonpos <- ✅ pow_le_one' | |
| ❌ AddCon.mk'_surjective <- ✅ Con.mk'_surjective | |
| ❌ sub_lt_sub_right <- ✅ div_lt_div_right' | |
| ❌ le_add_self <- ✅ le_mul_self | |
| ❌ Set.vadd_set_interᵢ₂_subset <- ✅ Set.smul_set_interᵢ₂_subset | |
| ❌ IsAddMonoidHom.neg <- ✅ IsMonoidHom.inv | |
| ❌ IsCentralVAdd.unop_vadd_eq_vadd <- ✅ IsCentralScalar.unop_smul_eq_smul | |
| ❌ Set.image_add_right' <- ✅ Set.image_mul_right' | |
| ❌ Set.op_vadd_inter_ne_empty_iff <- ✅ Set.op_smul_inter_ne_empty_iff | |
| ❌ Set.vadd_empty <- ✅ Set.smul_empty | |
| ❌ Right.nsmul_neg_iff <- ✅ Right.pow_lt_one_iff | |
| ❌ AddCon.neg <- ✅ Con.inv | |
| ❌ le_add_neg_iff_add_le <- ✅ le_mul_inv_iff_mul_le | |
| ❌ FreeAddMonoid.toList_add <- ✅ FreeMonoid.toList_mul | |
| ❌ Set.Nonempty.add <- ✅ Set.Nonempty.mul | |
| ❌ Set.Nonempty.vadd <- ✅ Set.Nonempty.smul | |
| ❌ Set.vadd_set_inter_subset <- ✅ Set.smul_set_inter_subset | |
| ❌ instVAddOrderDual' <- ✅ instSMulOrderDual' | |
| ❌ Part.add_get_eq <- ✅ Part.mul_get_eq | |
| ❌ le_of_add_le_left <- ✅ le_of_mul_le_left | |
| ❌ Set.sub_singleton <- ✅ Set.div_singleton | |
| ❌ Set.sub_empty <- ✅ Set.div_empty | |
| ❌ Set.not_zero_mem_sub_iff <- ✅ Set.not_one_mem_div_iff | |
| ❌ WithZero.add <- ✅ WithOne.mul | |
| ❌ Set.vadd_unionᵢ <- ✅ Set.smul_unionᵢ | |
| ❌ AddAction.bijective <- ✅ MulAction.bijective | |
| ❌ List.rel_sum <- ✅ List.rel_prod | |
| ❌ AddMonoidHom.ofClosureMEqTopLeft <- ✅ MonoidHom.ofClosureMEqTopLeft | |
| ❌ Set.addZeroClass <- ✅ Set.mulOneClass | |
| ❌ apply_abs_le_add_of_nonneg <- ✅ apply_abs_le_mul_of_one_le | |
| ❌ Set.vadd_mem_vadd <- ✅ Set.smul_mem_smul | |
| ❌ Set.zero <- ✅ Set.one | |
| ❌ AddCommMonoid.ext <- ✅ CommMonoid.ext | |
| ❌ apply_abs_le_add_of_nonneg' <- ✅ apply_abs_le_mul_of_one_le' | |
| ❌ max_neg_neg <- ✅ max_inv_inv' | |
| ❌ add_neg_neg_iff <- ✅ mul_inv_lt_one_iff | |
| ❌ le_iff_forall_pos_lt_add' <- ✅ le_iff_forall_one_lt_lt_mul' | |
| ❌ Set.vadd_inter_ne_empty_iff' <- ✅ Set.smul_inter_ne_empty_iff' | |
| ❌ AddEquiv.isAddGroupHom <- ✅ MulEquiv.isGroupHom | |
| ❌ LatticeOrderedCommGroup.pos_of_nonneg <- ✅ LatticeOrderedCommGroup.pos_of_one_le | |
| ❌ Part.add_mem_add <- ✅ Part.mul_mem_mul | |
| ❌ List.exists_mem_ne_zero_of_sum_ne_zero <- ✅ List.exists_mem_ne_one_of_prod_ne_one | |
| ❌ add_neg_lt_iff_lt_add <- ✅ mul_inv_lt_iff_lt_mul | |
| ❌ FreeAddMonoid.toList_ofList <- ✅ FreeMonoid.toList_ofList | |
| ❌ AddSubmonoid.nontrivial_iff <- ✅ Submonoid.nontrivial_iff | |
| ❌ Set.vadd_set_empty <- ✅ Set.smul_set_empty | |
| ❌ LatticeOrderedCommGroup.le_pos <- ✅ LatticeOrderedCommGroup.m_le_pos | |
| ❌ Fintype.decidableEqAddHomFintype <- ✅ Fintype.decidableEqMulHomFintype | |
| ❌ List.alternatingSum_cons_cons <- ✅ List.alternatingProd_cons_cons | |
| ❌ AddCon.kerLift_mk <- ✅ Con.kerLift_mk | |
| ❌ AddSubmonoid.coe_bot <- ✅ Submonoid.coe_bot | |
| ❌ WithBot.coe_pos <- ✅ WithBot.one_lt_coe | |
| ❌ AddSubsemigroup.add_mem_sup <- ✅ Subsemigroup.mul_mem_sup | |
| ❌ AddSemigroupPEmpty <- ✅ SemigroupPEmpty | |
| ❌ WithTop.coe_pos <- ✅ WithTop.one_lt_coe | |
| ❌ List.Perm.sum_eq <- ✅ List.Perm.prod_eq | |
| ❌ Set.inter_vadd_subset <- ✅ Set.inter_smul_subset | |
| ❌ Set.coe_singletonZeroHom <- ✅ Set.coe_singletonOneHom | |
| ❌ le_neg_iff_add_nonpos_right <- ✅ le_inv_iff_mul_le_one_right | |
| ❌ sub_le_neg_add_iff <- ✅ div_le_inv_mul_iff | |
| ❌ List.sum_reverse_noncomm <- ✅ List.prod_reverse_noncomm | |
| ❌ abs_eq_sup_neg <- ✅ abs_eq_sup_inv | |
| ❌ le_of_add_le_right <- ✅ le_of_mul_le_right | |
| ❌ List.alternatingSum_nil <- ✅ List.alternatingProd_nil | |
| ❌ AddAction.supports_of_mem <- ✅ MulAction.supports_of_mem | |
| ❌ List.sum_eq_zero <- ✅ List.prod_eq_one | |
| ❌ Multiset.sum_cons <- ✅ Multiset.prod_cons | |
| ❌ AddEquiv.isAddHom <- ✅ MulEquiv.isMulHom | |
| ❌ AddCon.addCommMonoid <- ✅ Con.commMonoid | |
| ❌ FreeAddMonoid.lift_of_comp_eq_map <- ✅ FreeMonoid.lift_of_comp_eq_map | |
| ❌ le_add_neg_iff_le <- ✅ le_mul_inv_iff_le | |
| ❌ Function.update_vadd <- ✅ Function.update_smul | |
| ❌ Multiset.sum <- ✅ Multiset.prod | |
| ❌ WithTop.zero_ne_top <- ✅ WithTop.one_ne_top | |
| ❌ AddOpposite.rec' <- ✅ MulOpposite.rec' | |
| ❌ IsAddGroupHom.id <- ✅ IsGroupHom.id | |
| ❌ Set.univ_add <- ✅ Set.univ_mul | |
| ❌ List.sum_eq_smul_single <- ✅ List.prod_eq_pow_single | |
| ❌ instVAddOrderDual <- ✅ instSMulOrderDual | |
| ❌ Function.vaddCommClass <- ✅ Function.smulCommClass | |
| ❌ Pi.orderedAddCancelCommMonoid <- ✅ Pi.orderedCancelCommMonoid | |
| ❌ Set.add_image_prod <- ✅ Set.image_mul_prod | |
| ❌ AddSubmonoid.center_to_add_subsemigroup <- ✅ Submonoid.center_toSubsemigroup | |
| ❌ sub_nonpos <- ✅ div_le_one' | |
| ❌ AddCommute.list_sum_right <- ✅ Commute.list_prod_right | |
| ❌ add_neg_le_add_neg_iff <- ✅ mul_inv_le_mul_inv_iff' | |
| ❌ Set.neg_mem_neg <- ✅ Set.inv_mem_inv | |
| ❌ VAddAssocClass.of_vadd_zero_add <- ✅ IsScalarTower.of_smul_one_mul | |
| ❌ List.length_pos_of_sum_pos <- ✅ List.length_pos_of_one_lt_prod | |
| ❌ Function.Injective.addAction <- ✅ Function.Injective.mulAction | |
| ❌ AddMonoidHom.compl₂ <- ✅ MonoidHom.compl₂ | |
| ❌ AddSubmonoid.coe_infᵢ <- ✅ Submonoid.coe_infᵢ | |
| ❌ StrictMono.neg <- ✅ StrictMono.inv | |
| ❌ FreeAddMonoid.lift_comp_of <- ✅ FreeMonoid.lift_comp_of | |
| ❌ nsmul_lt_nsmul <- ✅ pow_lt_pow' | |
| ❌ FreeAddMonoid.of_vadd <- ✅ FreeMonoid.of_smul | |
| ❌ List.sum_le_sum <- ✅ List.prod_le_prod' | |
| ❌ Set.sub_mem_sub <- ✅ Set.div_mem_div | |
| ❌ AddSemiconjBy <- ✅ SemiconjBy | |
| ❌ LatticeOrderedCommGroup.sup_eq_add_pos_sub <- ✅ LatticeOrderedCommGroup.sup_eq_mul_pos_div | |
| ❌ VAdd.comp.vaddCommClass <- ✅ SMul.comp.smulCommClass | |
| ❌ Set.add_singleton <- ✅ Set.mul_singleton | |
| ❌ le_cinfᵢ_add_cinfᵢ <- ✅ le_cinfᵢ_mul_cinfᵢ | |
| ❌ le_sub_iff_add_le' <- ✅ le_div_iff_mul_le' | |
| ❌ Set.vadd <- ✅ Set.smul | |
| ❌ List.alternatingSum_append <- ✅ List.alternatingProd_append | |
| ❌ LatticeOrderedCommGroup.add_inf_eq_add_inf_add <- ✅ LatticeOrderedCommGroup.mul_inf_eq_mul_inf_mul | |
| ❌ Set.mem_vadd_set <- ✅ Set.mem_smul_set | |
| ❌ AddSubsemigroup.mem_supᵢ_of_directed <- ✅ Subsemigroup.mem_supᵢ_of_directed | |
| ❌ LatticeOrderedCommGroup.neg_of_nonneg <- ✅ LatticeOrderedCommGroup.neg_of_one_le | |
| ❌ Set.sub_subset_sub_right <- ✅ Set.div_subset_div_right | |
| ❌ Right.self_le_neg <- ✅ Right.self_le_inv | |
| ❌ AddMonoidHom.coe_of <- ✅ MonoidHom.coe_of | |
| ❌ le_of_forall_pos_le_add <- ✅ le_of_forall_one_lt_le_mul | |
| ❌ AddCommSemigroup.IsRightCancelAdd.toIsLeftCancelAdd <- ✅ CommSemigroup.IsRightCancelMul.toIsLeftCancelMul | |
| ❌ Set.nsmul_subset_nsmul_of_zero_mem <- ✅ Set.pow_subset_pow_of_one_mem | |
| ❌ Set.mem_zero <- ✅ Set.mem_one | |
| ❌ Set.neg_empty <- ✅ Set.inv_empty | |
| ❌ Fintype.decidableEqZeroHomFintype <- ✅ Fintype.decidableEqOneHomFintype | |
| ❌ Set.singleton_vadd <- ✅ Set.singleton_smul | |
| ❌ Set.singleton_sub <- ✅ Set.singleton_div | |
| ❌ le_map_sub_add_map_sub <- ✅ le_map_div_add_map_div | |
| ❌ VAddCommClass.op_left <- ✅ SMulCommClass.op_left | |
| ❌ IsAddGroupHom.to_isAddMonoidHom <- ✅ IsGroupHom.to_isMonoidHom | |
| ❌ Set.vadd_subset_iff <- ✅ Set.smul_subset_iff | |
| ❌ AddCancelCommMonoid.toAddCancelMonoid <- ✅ CancelCommMonoid.toCancelMonoid | |
| ❌ Set.sub_subset_sub_left <- ✅ Set.div_subset_div_left | |
| ❌ add_neg_nonpos_iff <- ✅ mul_inv_le_one_iff | |
| ❌ max_zero_sub_max_neg_zero_eq_self <- ✅ max_one_div_max_inv_one_eq_self | |
| ❌ sub_le_self_iff <- ✅ div_le_self_iff | |
| ❌ Set.unionᵢ_sub_left_image <- ✅ Set.unionᵢ_div_left_image | |
| ❌ zsmul_neg <- ✅ inv_zpow | |
| ❌ AddCommute.vadd_left <- ✅ Commute.smul_left | |
| ❌ LatticeOrderedCommGroup.pos_eq_neg_neg <- ✅ LatticeOrderedCommGroup.pos_eq_neg_inv | |
| ❌ LatticeOrderedCommGroup.neg_nonneg <- ✅ LatticeOrderedCommGroup.one_le_neg | |
| ❌ Left.self_le_neg <- ✅ Left.self_le_inv | |
| ❌ lt_add_neg_iff_lt <- ✅ lt_mul_inv_iff_lt | |
| ❌ Set.sub_unionᵢ <- ✅ Set.div_unionᵢ | |
| ❌ Multiset.sum_map_erase <- ✅ Multiset.prod_map_erase | |
| ❌ vadd_left_cancel <- ✅ smul_left_cancel | |
| ❌ lt_or_lt_of_add_lt_add <- ✅ lt_or_lt_of_mul_lt_mul | |
| ❌ AddAction.toFun_apply <- ✅ MulAction.toFun_apply | |
| ❌ AddMonoidHom.isAddGroupHom <- ✅ MonoidHom.isGroupHom | |
| ❌ Set.vadd_subset_vadd_left <- ✅ Set.smul_subset_smul_left | |
| ❌ Function.const_nonpos_of_nonpos <- ✅ Function.const_le_one_of_le_one | |
| ❌ Set.singletonAddMonoidHom_apply <- ✅ Set.singletonMonoidHom_apply | |
| ❌ AddCon.lift_comp_mk' <- ✅ Con.lift_comp_mk' | |
| ❌ List.sum_map_eq_smul_single <- ✅ List.prod_map_eq_pow_single | |
| ❌ IsAddUnit.addSubmonoid <- ✅ IsUnit.submonoid | |
| ❌ AddSubmonoid.mem_supᵢ <- ✅ Submonoid.mem_supᵢ | |
| ❌ sub_lt_sub <- ✅ div_lt_div'' | |
| ❌ AddSubmonoid.closure_univ <- ✅ Submonoid.closure_univ | |
| ❌ Set.preimage_add_preimage_subset <- ✅ Set.preimage_mul_preimage_subset | |
| ❌ neg_add_le_iff_le_add' <- ✅ inv_mul_le_iff_le_mul' | |
| ❌ LatticeOrderedCommGroup.neg_zero <- ✅ LatticeOrderedCommGroup.neg_one | |
| ❌ AddLeftCancelSemigroup.toIsLeftCancelAdd <- ✅ LeftCancelSemigroup.toIsLeftCancelMul | |
| ❌ Multiset.all_zero_of_le_zero_le_of_sum_eq_zero <- ✅ Multiset.all_one_of_le_one_le_of_prod_eq_one | |
| ❌ Multiset.sum_map_le_sum <- ✅ Multiset.prod_map_le_prod | |
| ❌ Set.univ_add_univ <- ✅ Set.univ_mul_univ | |
| ❌ IsAddHom.to_isAddMonoidHom <- ✅ IsMulHom.to_isMonoidHom | |
| ❌ vadd_add_vadd <- ✅ smul_mul_smul | |
| ❌ List.sum_set <- ✅ List.prod_set | |
| ❌ AddCon.mem_coe <- ✅ Con.mem_coe | |
| ❌ min_le_add_of_nonneg_right <- ✅ min_le_mul_of_one_le_right | |
| ❌ AddCon.quotientKerEquivOfRightInverse <- ✅ Con.quotientKerEquivOfRightInverse | |
| ❌ vadd_vadd <- ✅ smul_smul | |
| ❌ AddRightCancelMonoid.faithfulVAdd <- ✅ RightCancelMonoid.faithfulSMul | |
| ❌ Set.vadd_eq_empty <- ✅ Set.smul_eq_empty | |
| ❌ Multiset.sum_hom_rel <- ✅ Multiset.prod_hom_rel | |
| ❌ nsmul_le_nsmul_of_nonpos <- ✅ pow_le_pow_of_le_one' | |
| ❌ AddSubsemigroup.coe_supₛ_of_directed_on <- ✅ Subsemigroup.coe_supₛ_of_directed_on | |
| ❌ add_ite <- ✅ mul_ite | |
| ❌ Set.unionᵢ_vadd_eq_setOf_exists <- ✅ Set.unionᵢ_smul_eq_setOf_exists | |
| ❌ lt_sub_iff_add_lt' <- ✅ lt_div_iff_mul_lt' | |
| ❌ sub_lt_sub_left <- ✅ div_lt_div_left' | |
| ❌ OrderEmbedding.addRight <- ✅ OrderEmbedding.mulRight | |
| ❌ sub_le_comm <- ✅ div_le_comm | |
| ❌ Set.range_vadd_range <- ✅ Set.range_smul_range | |
| ❌ Multiset.sum_singleton <- ✅ Multiset.prod_singleton | |
| ❌ Set.add_unionᵢ₂ <- ✅ Set.mul_unionᵢ₂ | |
| ❌ unique_zero <- ✅ unique_one | |
| ❌ IsAddGroupHom.map_zero <- ✅ IsGroupHom.map_one | |
| ❌ Sigma.vadd_mk <- ✅ Sigma.smul_mk | |
| ❌ Set.image_zero <- ✅ Set.image_one | |
| ❌ min_zero <- ✅ min_one | |
| ❌ Multiset.sum_toList <- ✅ Multiset.prod_toList | |
| ❌ Set.interᵢ_neg <- ✅ Set.interᵢ_inv | |
| ❌ Function.Injective.linearOrderedAddCommMonoid <- ✅ Function.Injective.linearOrderedCommMonoid | |
| ❌ List.card_nsmul_le_sum <- ✅ List.pow_card_le_prod | |
| ❌ EckmannHilton.addCommGroup <- ✅ EckmannHilton.commGroup | |
| ❌ vadd_eq_self_of_preimage_zsmul_eq_self <- ✅ smul_eq_self_of_preimage_zpow_eq_self | |
| ❌ LatticeOrderedCommGroup.pos_nonneg <- ✅ LatticeOrderedCommGroup.one_le_pos | |
| ❌ AddMonoidHom.map_one₂ <- ✅ MonoidHom.map_one₂ | |
| ❌ sub_pos <- ✅ one_lt_div' | |
| ❌ AddUnits.val_le_val <- ✅ Units.val_le_val | |
| ❌ List.SublistForall₂.sum_le_sum <- ✅ List.SublistForall₂.prod_le_prod' | |
| ❌ FreeAddMonoid.ofList_toList <- ✅ FreeMonoid.ofList_toList | |
| ❌ Set.preimage_add_left_zero <- ✅ Set.preimage_mul_left_one | |
| ❌ add_lt_add_iff_of_le_of_le <- ✅ mul_lt_mul_iff_of_le_of_le | |
| ❌ Function.const_nonpos <- ✅ Function.const_le_one | |
| ❌ neg_add_nonpos_iff <- ✅ inv_mul_le_one_iff | |
| ❌ Set.sub_eq_empty <- ✅ Set.div_eq_empty | |
| ❌ min_add_distrib' <- ✅ min_mul_distrib' | |
| ❌ vadd_vadd_vadd_comm <- ✅ smul_smul_smul_comm | |
| ❌ AddSubmonoid.mem_bot <- ✅ Submonoid.mem_bot | |
| ❌ List.sum_take_succ <- ✅ List.prod_take_succ | |
| ❌ OrderedAddCommGroup.to_contravariantClass_left_le <- ✅ OrderedCommGroup.to_contravariantClass_left_le | |
| ❌ Set.sub_inter_subset <- ✅ Set.div_inter_subset | |
| ❌ Set.isAddUnit_iff <- ✅ Set.isUnit_iff | |
| ❌ Set.Nonempty.of_sub_right <- ✅ Set.Nonempty.of_div_right | |
| ❌ IsAddMonoidHom.map_add' <- ✅ IsMonoidHom.map_mul' | |
| ❌ min_sub_sub_left <- ✅ min_div_div_left' | |
| ❌ List.Forall₂.sum_le_sum <- ✅ List.Forall₂.prod_le_prod' | |
| ❌ AddAut <- ✅ MulAut | |
| ❌ FreeAddMonoid.toList_of <- ✅ FreeMonoid.toList_of | |
| ❌ Sum.vadd_inr <- ✅ Sum.smul_inr | |
| ❌ Function.Injective.orderedAddCommGroup <- ✅ Function.Injective.orderedCommGroup | |
| ❌ Function.hasVAdd <- ✅ Function.hasSMul | |
| ❌ Set.sub_union <- ✅ Set.div_union | |
| ❌ AddSubmonoid.closure_eq_of_le <- ✅ Submonoid.closure_eq_of_le | |
| ❌ List.sum_join <- ✅ List.prod_join | |
| ❌ List.sum_map_hom <- ✅ List.prod_map_hom | |
| ❌ sub_le_sub <- ✅ div_le_div'' | |
| ❌ vadd_add_assoc <- ✅ smul_mul_assoc | |
| ❌ Set.addMonoid <- ✅ Set.monoid | |
| ❌ Sum.FaithfulVAddRight <- ✅ Sum.FaithfulSMulRight | |
| ❌ AddAction.surjective_vadd <- ✅ MulAction.surjective_smul | |
| ❌ Set.image_add_right <- ✅ Set.image_mul_right | |
| ❌ Set.mem_sub <- ✅ Set.mem_div | |
| ❌ Set.Nonempty.zero_mem_sub <- ✅ Set.Nonempty.one_mem_div | |
| ❌ neg_add_neg_iff <- ✅ inv_mul_lt_one_iff | |
| ❌ Set.add_eq_zero_iff <- ✅ Set.mul_eq_one_iff | |
| ❌ List.sum_lt_sum <- ✅ List.prod_lt_prod' | |
| ❌ LatticeOrderedCommGroup.hasZeroLatticeHasNegPart <- ✅ LatticeOrderedCommGroup.hasOneLatticeHasNegPart | |
| ❌ Pi.instPow -> ✅ Pi.instSMul | |
| ❌ Set.add_image_prod <- ✅ Set.image_div_prod | |
| ❌ nsmul_nonneg <- ✅ one_le_pow_of_one_le' | |
| ❌ Set.add_subset_add_right <- ✅ Set.mul_subset_mul_right | |
| ❌ AddMonoidHom.eq_of_eqOn_denseM <- ✅ MonoidHom.eq_of_eqOn_denseM | |
| ❌ IsAddHom.comp <- ✅ IsMulHom.comp | |
| ❌ self_le_add_right <- ✅ self_le_mul_right | |
| ❌ AddEquiv.withZeroCongr_symm <- ✅ MulEquiv.withOneCongr_symm | |
| ❌ Function.const_pos <- ✅ Function.one_lt_const | |
| ❌ max_sub_sub_left <- ✅ max_div_div_left' | |
| ❌ Set.unionᵢ_add_left_image <- ✅ Set.unionᵢ_mul_left_image | |
| ❌ Set.set_vadd_subset_set_vadd_iff <- ✅ Set.set_smul_subset_set_smul_iff | |
| ❌ WithZero.zero <- ✅ WithOne.one | |
| ❌ Set.vadd_interᵢ₂_subset <- ✅ Set.smul_interᵢ₂_subset | |
| ❌ map_list_sum <- ✅ map_list_prod | |
| ❌ LatticeOrderedCommGroup.inf_eq_sub_pos_sub <- ✅ LatticeOrderedCommGroup.inf_eq_div_pos_div | |
| ❌ Set.vadd_interᵢ_subset <- ✅ Set.smul_interᵢ_subset | |
| ❌ le_add_right <- ✅ le_mul_right | |
| ❌ neg_vadd_vadd <- ✅ inv_smul_smul | |
| ❌ fn_min_add_fn_max <- ✅ fn_min_mul_fn_max | |
| ❌ VAddCommClass.symm <- ✅ SMulCommClass.symm | |
| ❌ Set.vadd_set_mono <- ✅ Set.smul_set_mono | |
| ❌ Multiset.sum_map_add <- ✅ Multiset.prod_map_mul | |
| ❌ AddSemiconjBy.eq <- ✅ SemiconjBy.eq | |
| ❌ Set.image2_sub <- ✅ Set.image2_div | |
| ❌ sub_nonneg <- ✅ one_le_div' | |
| ❌ AddSubmonoid.closure_mono <- ✅ Submonoid.closure_mono | |
| ❌ FreeAddMonoid.ofList_nil <- ✅ FreeMonoid.ofList_nil | |
| ❌ AddCon.ker_apply_eq_preimage <- ✅ Con.ker_apply_eq_preimage | |
| ❌ Set.inter_sub_subset <- ✅ Set.inter_div_subset | |
| ❌ AddCon.smulinst <- ✅ Con.smulinst | |
| ❌ le_cinfᵢ_add <- ✅ le_cinfᵢ_mul | |
| ❌ WithTop.coe_zero <- ✅ WithTop.coe_one | |
| ❌ Multiset.card_nsmul_le_sum <- ✅ Multiset.pow_card_le_prod | |
| ❌ AddMonoidHom.map_inv₂ <- ✅ MonoidHom.map_inv₂ | |
| ❌ Set.inter_neg <- ✅ Set.inter_inv | |
| ❌ IsAddUnit.mem_addSubmonoid_iff <- ✅ IsUnit.mem_submonoid_iff | |
| ❌ lt_sub_iff_add_lt <- ✅ lt_div_iff_mul_lt | |
| ❌ AddAction.toPerm <- ✅ MulAction.toPerm | |
| ❌ IsAddMonoidHom.comp <- ✅ IsMonoidHom.comp | |
| ❌ FreeAddMonoid.recOn_of_add <- ✅ FreeMonoid.recOn_of_mul | |
| ❌ List.sum_range_succ <- ✅ List.prod_range_succ | |
| ❌ AddCon.addGroup <- ✅ Con.group | |
| ❌ FreeAddMonoid.of_injective <- ✅ FreeMonoid.of_injective | |
| ❌ AddCommMonoid.toAddMonoid_injective <- ✅ CommMonoid.toMonoid_injective | |
| ❌ zero_min <- ✅ one_min | |
| ❌ vadd_neg_vadd <- ✅ smul_inv_smul | |
| ❌ Set.image_add <- ✅ Set.image_mul | |
| ❌ AddSubmonoid.ext <- ✅ Submonoid.ext | |
| ❌ AddAction.Supports <- ✅ MulAction.Supports | |
| ❌ AddCancelMonoid.ext <- ✅ CancelMonoid.ext | |
| ❌ FreeAddMonoid.comp_lift <- ✅ FreeMonoid.comp_lift | |
| ❌ max_add_add_right <- ✅ max_mul_mul_right | |
| ❌ Set.zero_nonempty <- ✅ Set.one_nonempty | |
| ❌ Multiset.le_sum_of_mem <- ✅ Multiset.le_prod_of_mem | |
| ❌ sub_le_sub_iff <- ✅ div_le_div_iff' | |
| ❌ AddUnits.max_val <- ✅ Units.max_val | |
| ❌ AddSemigroup.isScalarTower <- ✅ Semigroup.isScalarTower | |
| ❌ WithBot.map_zero <- ✅ WithBot.map_one | |
| ❌ AddUnits.val_sub_eq_sub_val <- ✅ Units.val_div_eq_div_val | |
| ❌ Part.left_dom_of_add_dom <- ✅ Part.left_dom_of_mul_dom | |
| ❌ le_map_sub_add_map_sub <- ✅ le_map_div_mul_map_div | |
| ❌ neg_sup_eq_neg_inf_neg <- ✅ inv_sup_eq_inv_inf_inv | |
| ❌ Set.singletonZeroHom <- ✅ Set.singletonOneHom | |
| ❌ List.sum_range_succ' <- ✅ List.prod_range_succ' | |
| ❌ FreeAddMonoid.lift_eval_of <- ✅ FreeMonoid.lift_eval_of | |
| ❌ lt_add_neg_iff_add_lt <- ✅ lt_mul_inv_iff_mul_lt | |
| ❌ WithTop.coe_eq_zero <- ✅ WithTop.coe_eq_one | |
| ❌ Function.Surjective.addAction <- ✅ Function.Surjective.mulAction | |
| ❌ bot_eq_zero' <- ✅ bot_eq_one' | |
| ❌ FreeAddMonoid.toList_of_add <- ✅ FreeMonoid.toList_of_mul | |
| ❌ AddSubsemigroup.mem_sup_left <- ✅ Subsemigroup.mem_sup_left | |
| ❌ List.sum_erase <- ✅ List.prod_erase | |
| ❌ FreeAddMonoid.ofList_symm <- ✅ FreeMonoid.ofList_symm | |
| ❌ VAddAssocClass.op_right <- ✅ IsScalarTower.op_right | |
| ❌ IsAddHom.neg <- ✅ IsMulHom.inv | |
| ❌ AddEquiv.withZeroCongr_trans <- ✅ MulEquiv.withOneCongr_trans | |
| ❌ Set.neg_mem_Ioc_iff <- ✅ Set.inv_mem_Ioc_iff | |
| ❌ List.eq_of_sum_take_eq <- ✅ List.eq_of_prod_take_eq | |
| ❌ add_vadd_zero <- ✅ mul_smul_one | |
| ❌ Set.neg_range <- ✅ Set.inv_range | |
| ❌ Right.neg_neg_iff <- ✅ Right.inv_lt_one_iff | |
| ❌ FreeAddMonoid.ofList_cons <- ✅ FreeMonoid.ofList_cons | |
| ❌ AddSubmonoid.closure_eq <- ✅ Submonoid.closure_eq | |
| ❌ map_zsmul' <- ✅ map_zpow' | |
| ❌ AddSubmonoid.coe_top <- ✅ Submonoid.coe_top | |
| ❌ sub_le_sub_right <- ✅ div_le_div_right' | |
| ❌ Right.neg_nonpos_iff <- ✅ Right.inv_le_one_iff | |
| ❌ Multiset.sum_map_neg' <- ✅ Multiset.prod_map_inv' | |
| ❌ AddMonoid.ext <- ✅ Monoid.ext | |
| ❌ Set.Nonempty.subset_zero_iff <- ✅ Set.Nonempty.subset_one_iff | |
| ❌ AddCon.nsmul <- ✅ Con.pow | |
| ❌ Set.Nonempty.of_sub_left <- ✅ Set.Nonempty.of_div_left | |
| ❌ AddCon.kerLift_range_eq <- ✅ Con.kerLift_range_eq | |
| ❌ AddCon.vadd <- ✅ Con.smul | |
| ❌ Set.addSemigroup <- ✅ Set.semigroup | |
| ❌ add_neg_lt_iff_le_add' <- ✅ mul_inv_lt_iff_le_mul' | |
| ❌ AddMonoidHom.coe_ofClosureMEqTopLeft <- ✅ MonoidHom.coe_ofClosureMEqTopLeft | |
| ❌ Set.union_neg <- ✅ Set.union_inv | |
| ❌ List.sum_neg_reverse <- ✅ List.prod_inv_reverse | |
| ❌ self_le_add_left <- ✅ self_le_mul_left | |
| ❌ lt_neg <- ✅ lt_inv' | |
| ❌ VAddAssocClass.left <- ✅ IsScalarTower.left | |
| ❌ AddCommSemigroup.IsLeftCancelAdd.toIsRightCancelAdd <- ✅ CommSemigroup.IsLeftCancelMul.toIsRightCancelMul | |
| ❌ ofNat_zsmul <- ✅ zpow_ofNat | |
| ❌ AddCon.lift_funext <- ✅ Con.lift_funext | |
| ❌ FreeAddMonoid.toList_map <- ✅ FreeMonoid.toList_map | |
| ❌ FreeAddMonoid.mkAddAction <- ✅ FreeMonoid.mkMulAction | |
| ❌ lt_neg_iff_add_neg' <- ✅ lt_inv_iff_mul_lt_one' | |
| ❌ map_zsmul <- ✅ map_zpow | |
| ❌ vaddCommClass_self <- ✅ smulCommClass_self | |
| ❌ zero_vadd <- ✅ one_smul | |
| ❌ LatticeOrderedCommGroup.sup_sub_inf_eq_abs_sub <- ✅ LatticeOrderedCommGroup.sup_div_inf_eq_abs_div | |
| ❌ Left.neg_neg_iff <- ✅ Left.inv_lt_one_iff | |
| ❌ Set.singleton_sub_singleton <- ✅ Set.singleton_div_singleton | |
| ❌ Set.preimage_vadd <- ✅ Set.preimage_smul | |
| ❌ Set.addCommMonoid <- ✅ Set.commMonoid | |
| ❌ Set.vaddCommClass_set <- ✅ Set.smulCommClass_set | |
| ❌ vaddZeroHom <- ✅ smulOneHom | |
| ❌ zsmul_nonneg <- ✅ one_le_zpow | |
| ❌ LatticeOrderedCommGroup.pos_eq_self_of_pos_pos <- ✅ LatticeOrderedCommGroup.pos_eq_self_of_one_lt_pos | |
| ❌ Set.vadd_set_union <- ✅ Set.smul_set_union | |
| ❌ OrderMonoidHom.comp_apply -> ✅ OrderAddMonoidHom.comp_apply | |
| ❌ AddSubmonoid.zero_mem <- ✅ Submonoid.one_mem | |
| ❌ Set.empty_sub <- ✅ Set.empty_div | |
| ❌ Part.right_dom_of_sub_dom <- ✅ Part.right_dom_of_div_dom | |
| ❌ Set.preimage_vadd_neg <- ✅ Set.preimage_smul_inv | |
| ❌ max_le_add_of_nonneg <- ✅ max_le_mul_of_one_le | |
| ❌ Set.sub_subset_sub <- ✅ Set.div_subset_div | |
| ❌ Left.self_lt_neg <- ✅ Left.self_lt_inv | |
| ❌ FreeAddMonoid.ofList_join <- ✅ FreeMonoid.ofList_join | |
| ❌ Set.singletonAddHom <- ✅ Set.singletonMulHom | |
| ❌ max_add_add_left <- ✅ max_mul_mul_left | |
| ❌ smul_eq_zero_iff <- ✅ pow_eq_one_iff | |
| ❌ IsAddHom.id <- ✅ IsMulHom.id | |
| ❌ add_neg_lt_add_neg_iff <- ✅ mul_inv_lt_mul_inv_iff' | |
| ❌ Pi.orderedAddCommMonoid <- ✅ Pi.orderedCommMonoid | |
| ❌ neg_nonpos_of_nonneg <- ✅ inv_le_one_of_one_le | |
| ❌ AddCon.addCommSemigroup <- ✅ Con.commSemigroup | |
| ❌ csupᵢ_add_le <- ✅ csupᵢ_mul_le | |
| ❌ Set.mem_neg_vadd_set_iff <- ✅ Set.mem_inv_smul_set_iff | |
| ❌ nsmul_le_nsmul_of_le_right <- ✅ pow_le_pow_of_le_left' | |
| ❌ IsAddGroupHom.neg <- ✅ IsGroupHom.inv | |
| ❌ Neg.isAddGroupHom <- ✅ Inv.isGroupHom | |
| ❌ Set.add_image_prod <- ✅ Set.image_smul_prod | |
| ❌ AddCommute.list_sum_left <- ✅ Commute.list_prod_left | |
| ❌ nsmul_le_nsmul <- ✅ pow_le_pow' | |
| ❌ sub_lt_sub_iff <- ✅ div_lt_div_iff' | |
| ❌ AddSubmonoid.mem_mk <- ✅ Submonoid.mem_mk | |
| ❌ map_multiset_sum <- ✅ map_multiset_prod | |
| ❌ Part.neg_some <- ✅ Part.inv_some | |
| ❌ AddSemiconjBy.function_semiconj_add_right_swap <- ✅ SemiconjBy.function_semiconj_mul_right_swap | |
| ❌ Set.coe_singletonAddMonoidHom <- ✅ Set.coe_singletonMonoidHom | |
| ❌ List.length_pos_of_sum_ne_zero <- ✅ List.length_pos_of_prod_ne_one | |
| ❌ Set.addAction <- ✅ Set.mulAction | |
| ❌ Set.piecewise_vadd <- ✅ Set.piecewise_smul | |
| ❌ WithTop.coe_lt_zero <- ✅ WithTop.coe_lt_one | |
| ❌ Right.neg_le_self <- ✅ Right.inv_le_self | |
| ❌ LatticeOrderedCommGroup.pos_part_def <- ✅ LatticeOrderedCommGroup.m_pos_part_def | |
| ❌ LatticeOrderedCommGroup.pos_nonpos_iff <- ✅ LatticeOrderedCommGroup.pos_le_one_iff | |
| ❌ Set.vadd_set_sdiff <- ✅ Set.smul_set_sdiff | |
| ❌ Set.image2_add <- ✅ Set.image2_mul | |
| ❌ Set.vaddCommClass_set' <- ✅ Set.smulCommClass_set' | |
| ❌ VAddCommClass.opposite_mid <- ✅ SMulCommClass.opposite_mid | |
| ❌ arrowAddAction <- ✅ arrowAction | |
| ❌ AddMonoidHom.ofMapAddNeg <- ✅ MonoidHom.ofMapMulInv | |
| ❌ VAdd.comp.isScalarTower <- ✅ SMul.comp.isScalarTower | |
| ❌ Set.union_vadd <- ✅ Set.union_smul | |
| ❌ neg_le_neg_iff <- ✅ inv_le_inv_iff | |
| ❌ Set.preimage_add_right_singleton <- ✅ Set.preimage_mul_right_singleton | |
| ❌ AddCommGroup.ext <- ✅ CommGroup.ext | |
| ❌ vadd_ite <- ✅ smul_ite | |
| ❌ FreeAddMonoid.toList_symm <- ✅ FreeMonoid.toList_symm | |
| ❌ AddMonoidHom.of <- ✅ MonoidHom.of | |
| ❌ Multiset.sum_induction_nonempty <- ✅ Multiset.prod_induction_nonempty | |
| ❌ Set.Nonempty.vadd_set <- ✅ Set.Nonempty.smul_set | |
| ❌ List.sum_set' <- ✅ List.prod_set' | |
| ❌ vadd_pi <- ✅ smul_pi | |
| ❌ LatticeOrderedCommGroup.neg_eq_neg_inf_zero <- ✅ LatticeOrderedCommGroup.neg_eq_inv_inf_one | |
| ❌ AddCon.coe_vadd <- ✅ Con.coe_smul | |
| ❌ AddCon.addMonoid <- ✅ Con.monoid | |
| ❌ Monotone.neg <- ✅ Monotone.inv | |
| ❌ List.sum_concat <- ✅ List.prod_concat | |
| ❌ AddCon.lift_unique <- ✅ Con.lift_unique | |
| ❌ Sum.vadd_def <- ✅ Sum.smul_def | |
| ❌ List.sum_singleton <- ✅ List.prod_singleton | |
| ❌ Prod.smul <- ✅ Prod.pow | |
| ❌ add_sup <- ✅ mul_sup | |
| ❌ Sigma.FaithfulVAdd' <- ✅ Sigma.FaithfulSMul' | |
| ❌ Set.isAddUnit_singleton <- ✅ Set.isUnit_singleton | |
| ❌ Set.bddAbove_add <- ✅ Set.bddAbove_mul | |
| ❌ AddSubmonoid.mem_carrier <- ✅ Submonoid.mem_carrier | |
| ❌ neg_inf_eq_sup_neg <- ✅ inv_inf_eq_sup_inv | |
| ❌ LatticeOrderedCommGroup.neg_eq_zero_iff <- ✅ LatticeOrderedCommGroup.neg_eq_one_iff | |
| ❌ FreeAddMonoid.ofList <- ✅ FreeMonoid.ofList | |
| ❌ LatticeOrderedCommGroup.pos_zero <- ✅ LatticeOrderedCommGroup.pos_one | |
| ❌ AddCommute.vadd_right <- ✅ Commute.smul_right | |
| ❌ IsAddMonoidHom.id <- ✅ IsMonoidHom.id | |
| ❌ List.sum_eq_zero_iff <- ✅ List.prod_eq_one_iff | |
| ❌ LatticeOrderedCommGroup.neg_of_inv_nonneg <- ✅ LatticeOrderedCommGroup.neg_of_one_le_inv | |
| ❌ LatticeOrderedCommGroup.hasZeroLatticeHasPosPart <- ✅ LatticeOrderedCommGroup.hasOneLatticeHasPosPart | |
| ❌ AddRightCancelMonoid.toAddMonoid_injective <- ✅ RightCancelMonoid.toMonoid_injective | |
| ❌ Multiset.sum_map_zsmul <- ✅ Multiset.prod_map_zpow | |
| ❌ VAddCommClass.op_right <- ✅ SMulCommClass.op_right | |
| ❌ AntitoneOn.neg <- ✅ AntitoneOn.inv | |
| ❌ Set.image2_vadd <- ✅ Set.image2_smul | |
| ❌ IsAddGroupHom.comp <- ✅ IsGroupHom.comp | |
| ❌ lt_sub_comm <- ✅ lt_div_comm | |
| ❌ ZeroHom.withBotMap <- ✅ OneHom.withBotMap | |
| ❌ AddMonoidHom.compHom <- ✅ MonoidHom.compHom | |
| ❌ neg_lt_neg <- ✅ inv_lt_inv' | |
| ❌ sub_le_sub_iff_right <- ✅ div_le_div_iff_right | |
| ❌ FreeAddMonoid.casesOn_zero <- ✅ FreeMonoid.casesOn_one | |
| ❌ AddAction.toPerm_injective <- ✅ MulAction.toPerm_injective | |
| ❌ Set.singletonAddHom_apply <- ✅ Set.singletonMulHom_apply | |
| ❌ AddCon.ker <- ✅ Con.ker | |
| ❌ neg_neg_of_pos <- ✅ inv_lt_one_of_one_lt | |
| ❌ Set.preimage_add_right_zero <- ✅ Set.preimage_mul_right_one | |
| ❌ AddMonoidHom.ofClosureMEqTopRight <- ✅ MonoidHom.ofClosureMEqTopRight | |
| ❌ List.sum_isAddUnit <- ✅ List.prod_isUnit | |
| ❌ AddSubmonoid.supᵢ_eq_closure <- ✅ Submonoid.supᵢ_eq_closure | |
| ❌ VAdd.comp.vadd <- ✅ SMul.comp.smul | |
| ❌ AddCommSemigroup.IsLeftCancelAdd.toIsCancelAdd <- ✅ CommSemigroup.IsLeftCancelMul.toIsCancelMul | |
| ❌ sub_lt_sub_iff_right <- ✅ div_lt_div_iff_right | |
| ❌ Set.zero_subset <- ✅ Set.one_subset | |
| ❌ AddSubsemigroup.mem_supₛ_of_directed_on <- ✅ Subsemigroup.mem_supₛ_of_directed_on | |
| ❌ min_le_add_of_nonneg_left <- ✅ min_le_mul_of_one_le_left | |
| ❌ Multiset.sum_le_sum_of_rel_le <- ✅ Multiset.prod_le_prod_of_rel_le | |
| ❌ Set.add_subset_iff <- ✅ Set.mul_subset_iff | |
| ❌ le_iff_forall_pos_lt_add <- ✅ le_iff_forall_one_lt_lt_mul | |
| ❌ List.monotone_sum_take <- ✅ List.monotone_prod_take | |
| ❌ AddSubmonoid.copy_eq <- ✅ Submonoid.copy_eq | |
| ❌ Set.coe_singletonAddHom <- ✅ Set.coe_singletonMulHom | |
| ❌ MonotoneOn.neg <- ✅ MonotoneOn.inv | |
| ❌ neg_lt_iff_pos_add <- ✅ inv_lt_iff_one_lt_mul | |
| ❌ neg_lt_iff_pos_add' <- ✅ inv_lt_iff_one_lt_mul' | |
| ❌ AddCommGroup.toAddGroup_injective <- ✅ CommGroup.toGroup_injective | |
| ❌ AddCon.ker_eq_lift_of_injective <- ✅ Con.ker_eq_lift_of_injective | |
| ❌ Set.unionᵢ_vadd <- ✅ Set.unionᵢ_smul | |
| ❌ AddSubmonoid.mk_le_mk <- ✅ Submonoid.mk_le_mk | |
| ❌ StrictMonoOn.neg <- ✅ StrictMonoOn.inv | |
| ❌ neg_le_sub_iff_le_add' <- ✅ inv_le_div_iff_le_mul' | |
| ❌ LatticeOrderedCommGroup.abs_sup_sub_sup_le_abs <- ✅ LatticeOrderedCommGroup.mabs_sup_div_sup_le_mabs | |
| ❌ LatticeOrderedCommGroup.neg_eq_zero_iff' <- ✅ LatticeOrderedCommGroup.neg_eq_one_iff' | |
| ❌ Set.subtractionCommMonoid <- ✅ Set.divisionCommMonoid | |
| ❌ Set.vadd_univ <- ✅ Set.smul_univ | |
| ❌ vadd_zero_vadd <- ✅ smul_one_smul | |
| ❌ ULift.addCancelCommMonoid <- ✅ ULift.cancelCommMonoid | |
| ❌ Set.vadd_nonempty <- ✅ Set.smul_nonempty | |
| ❌ FreeAddMonoid.ofList_singleton <- ✅ FreeMonoid.ofList_singleton | |
| ❌ Set.vadd_set_univ <- ✅ Set.smul_set_univ | |
| ❌ min_add_distrib <- ✅ min_mul_distrib | |
| ❌ AddCon.comap_eq <- ✅ Con.comap_eq | |
| ❌ StrictAnti.neg <- ✅ StrictAnti.inv | |
| ❌ Left.neg_nonpos_iff <- ✅ Left.inv_le_one_iff | |
| ❌ Set.vadd_set_singleton <- ✅ Set.smul_set_singleton | |
| ❌ Set.image_add_left' <- ✅ Set.image_mul_left' | |
| ❌ neg_add_lt_iff_lt_add <- ✅ inv_mul_lt_iff_lt_mul | |
| ❌ Set.subtractionMonoid <- ✅ Set.divisionMonoid | |
| ❌ List.all_zero_of_le_zero_le_of_sum_eq_zero <- ✅ List.all_one_of_le_one_le_of_prod_eq_one | |
| ❌ Multiset.sum_map_le_sum_map <- ✅ Multiset.prod_map_le_prod_map | |
| ❌ Set.vadd_set_range <- ✅ Set.smul_set_range | |
| ❌ Set.sub_unionᵢ₂ <- ✅ Set.div_unionᵢ₂ | |
| ❌ List.exists_le_of_sum_le <- ✅ List.exists_le_of_prod_le' | |
| ❌ FreeAddMonoid.toList <- ✅ FreeMonoid.toList | |
| ❌ sub_le_sub_left <- ✅ div_le_div_left' | |
| ❌ LinearOrderedAddCommGroup.to_covariantClass <- ✅ LinearOrderedCommGroup.to_covariantClass | |
| ❌ List.alternatingSum_cons_cons' <- ✅ List.alternatingProd_cons_cons' | |
| ❌ Set.image_op_neg <- ✅ Set.image_op_inv | |
| ❌ Multiset.smul_count <- ✅ Multiset.pow_count | |
| ❌ ite_add <- ✅ ite_mul | |
| ❌ List.alternatingSum_cons' <- ✅ List.alternatingProd_cons' | |
| ❌ AddGroup.ext <- ✅ Group.ext | |
| ❌ AddMonoidHom.isAddMonoidHom_coe <- ✅ MonoidHom.isMonoidHom_coe | |
| ❌ Set.neg_mem_Ioo_iff <- ✅ Set.inv_mem_Ioo_iff | |
| ❌ EckmannHilton.AddZeroClass.IsUnital <- ✅ EckmannHilton.MulOneClass.isUnital | |
| ❌ AddMonoid.toOppositeAddAction <- ✅ Monoid.toOppositeMulAction | |
| ❌ AddSubmonoid.closure_unionᵢ <- ✅ Submonoid.closure_unionᵢ | |
| ❌ VAddCommClass.of_add_vadd_zero <- ✅ SMulCommClass.of_mul_smul_one | |
| ❌ AddEquiv.isAddMonoidHom <- ✅ MulEquiv.isMonoidHom | |
| ❌ AddCon.to_addSubmonoid_inj <- ✅ Con.to_submonoid_inj | |
| ❌ List.sum_reverse <- ✅ List.prod_reverse | |
| ❌ AddMonoidHom.eval <- ✅ MonoidHom.eval | |
| ❌ AddCon.coe_mk' <- ✅ Con.coe_mk' | |
| ❌ le_iff_exists_add' <- ✅ le_iff_exists_mul' | |
| ❌ Set.unionᵢ_sub_right_image <- ✅ Set.unionᵢ_div_right_image | |
| ❌ nsmul_neg <- ✅ pow_lt_one' | |
| ❌ LatticeOrderedCommGroup.pos_add_neg <- ✅ LatticeOrderedCommGroup.pos_mul_neg | |
| ❌ AddMonoidHom.compHom' <- ✅ MonoidHom.compHom' | |
| ❌ LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub <- ✅ LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div | |
| ❌ Function.Injective.cancelMonoid -> ✅ Function.Injective.addCancelMonoid | |
| ❌ neg_le_iff_add_nonneg' <- ✅ inv_le_iff_one_le_mul' | |
| ❌ Multiset.sum_map_sub <- ✅ Multiset.prod_map_div | |
| ❌ Right.pow_neg <- ✅ Right.pow_lt_one_of_lt | |
| ❌ sub_lt_comm <- ✅ div_lt_comm | |
| ❌ Set.empty_add <- ✅ Set.empty_mul | |
| ❌ min_add_max <- ✅ min_mul_max | |
| ❌ FreeAddMonoid.of <- ✅ FreeMonoid.of | |
| ❌ AddSubmonoid.closure <- ✅ Submonoid.closure | |
| ❌ FreeAddMonoid.casesOn <- ✅ FreeMonoid.casesOn | |
| ❌ AddMonoidHom.coe_ofClosureMEqTopRight <- ✅ MonoidHom.coe_ofClosureMEqTopRight | |
| ❌ FreeAddMonoid.hom_map_lift <- ✅ FreeMonoid.hom_map_lift | |
| ❌ Set.vadd_union <- ✅ Set.smul_union | |
| ❌ smul_neg_iff <- ✅ pow_lt_one_iff | |
| ❌ LatticeOrderedCommGroup.abs_nonneg <- ✅ LatticeOrderedCommGroup.one_le_abs | |
| ❌ List.sum_add_sum_eq_sum_zipWith_of_length_eq <- ✅ List.prod_mul_prod_eq_prod_zipWith_of_length_eq | |
| ❌ sub_lt_sub_iff_left <- ✅ div_lt_div_iff_left | |
| ❌ Set.unionᵢ_add <- ✅ Set.unionᵢ_mul | |
| ❌ AddSubsemigroup.mem_supᵢ_of_mem <- ✅ Subsemigroup.mem_supᵢ_of_mem | |
| ❌ IsAddUnit.vadd_left_cancel <- ✅ IsUnit.smul_left_cancel | |
| ❌ Pi.orderedAddCommGroup <- ✅ Pi.orderedCommGroup | |
| ❌ Right.pow_nonpos <- ✅ Right.pow_le_one_of_le | |
| ❌ le_of_forall_pos_lt_add' <- ✅ le_of_forall_one_lt_lt_mul' | |
| ❌ add_eq_zero_iff <- ✅ mul_eq_one_iff | |
| ❌ neg_add_lt_iff_lt_add' <- ✅ inv_mul_lt_iff_lt_mul' | |
| ❌ Sum.vadd_swap <- ✅ Sum.smul_swap | |
| ❌ neg_add_neg_iff_lt <- ✅ inv_mul_lt_one_iff_lt | |
| ❌ Right.self_lt_neg <- ✅ Right.self_lt_inv | |
| ❌ LatticeOrderedCommGroup.neg_of_neg_nonpos <- ✅ LatticeOrderedCommGroup.neg_of_inv_le_one | |
| ❌ AddUnits.mk_val <- ✅ Units.mk_val | |
| ❌ nsmul_nonneg_iff <- ✅ one_le_pow_iff | |
| ❌ Set.vadd_inter_subset <- ✅ Set.smul_inter_subset | |
| ❌ Multiset.le_sum_nonempty_of_subadditive_on_pred <- ✅ Multiset.le_prod_nonempty_of_submultiplicative_on_pred | |
| ❌ List.sum_nil <- ✅ List.prod_nil | |
| ❌ IsAddGroupHom.map_sub <- ✅ IsGroupHom.map_div | |
| ❌ Multiset.sum_hom <- ✅ Multiset.prod_hom | |
| ❌ FreeAddMonoid.lift_symm_apply <- ✅ FreeMonoid.lift_symm_apply | |
| ❌ nsmul_strictMono_right <- ✅ pow_strictMono_left | |
| ❌ List.sum_nonneg <- ✅ List.one_le_prod_of_one_le | |
| ❌ AddSemiconjBy.map <- ✅ SemiconjBy.map | |
| ❌ Set.unionᵢ_add_right_image <- ✅ Set.unionᵢ_mul_right_image | |
| ❌ LinearOrderedAddCommGroup.to_noMinOrder <- ✅ LinearOrderedCommGroup.to_noMinOrder | |
| ❌ vadd_zero_add <- ✅ smul_one_mul | |
| ❌ Set.subset_set_vadd_iff <- ✅ Set.subset_set_smul_iff | |
| ❌ Multiset.sum_eq_zero_iff <- ✅ Multiset.prod_eq_one_iff | |
| ❌ Set.unionᵢ_sub <- ✅ Set.unionᵢ_div | |
| ❌ Multiset.sum_map_eq_smul_single <- ✅ Multiset.prod_map_eq_pow_single | |
| ❌ FreeAddMonoid.recOn <- ✅ FreeMonoid.recOn | |
| ❌ LatticeOrderedCommGroup.abs_abs <- ✅ LatticeOrderedCommGroup.mabs_mabs | |
| ❌ AddCommSemigroup.to_isCommutative <- ✅ CommSemigroup.to_isCommutative | |
| ❌ Add.toVAdd <- ✅ Mul.toSMul | |
| ❌ AddSubmonoid.closure_empty <- ✅ Submonoid.closure_empty | |
| ❌ le_add_left <- ✅ le_mul_left | |
| ❌ FreeAddMonoid.map_id <- ✅ FreeMonoid.map_id | |
| ❌ Multiset.sum_add <- ✅ Multiset.prod_add | |
| ❌ AddOpposite.op_sub <- ✅ MulOpposite.op_div | |
| ❌ Set.vadd_set_nonempty <- ✅ Set.smul_set_nonempty | |
| ❌ AddCon.quotientKerEquivRange <- ✅ Con.quotientKerEquivRange | |
| ❌ Set.neg <- ✅ Set.inv | |
| ❌ AddCon.comapQuotientEquiv <- ✅ Con.comapQuotientEquiv | |
| ❌ LatticeOrderedCommGroup.le_iff_pos_le_neg_ge <- ✅ LatticeOrderedCommGroup.m_le_iff_pos_le_neg_ge | |
| ❌ Set.unionᵢ_vadd_left_image <- ✅ Set.unionᵢ_smul_left_image | |
| ❌ AddSubsemigroup.mem_sup_right <- ✅ Subsemigroup.mem_sup_right | |
| ❌ AddSemiconjBy.add_right <- ✅ SemiconjBy.mul_right | |
| ❌ AddMonoidHom.compr₂ <- ✅ MonoidHom.compr₂ | |
| ❌ smul_mem <- ✅ pow_mem | |
| ❌ Set.image_add_left <- ✅ Set.image_mul_left | |
| ❌ Set.union_sub <- ✅ Set.union_div | |
| ❌ sub_le_iff_le_add' <- ✅ div_le_iff_le_mul' | |
| ❌ List.sum_eq_foldr <- ✅ List.prod_eq_foldr | |
| ❌ OneHom.map_one' -> ✅ ZeroHom.map_zero' | |
| ❌ vadd_univ_pi <- ✅ smul_univ_pi | |
| ❌ min_sub_sub_right <- ✅ min_div_div_right' | |
| ❌ Set.subset_add_right <- ✅ Set.subset_mul_right | |
| ❌ Part.some_add_some <- ✅ Part.some_mul_some | |
| ❌ LatticeOrderedCommGroup.neg_abs <- ✅ LatticeOrderedCommGroup.m_neg_abs | |
| ❌ LatticeOrderedCommGroup.neg_le_abs <- ✅ LatticeOrderedCommGroup.inv_le_abs | |
| ❌ comp_vadd_left <- ✅ comp_smul_left | |
| ❌ AddCon.lift_mk' <- ✅ Con.lift_mk' | |
| ❌ Function.Injective.orderedAddCommMonoid <- ✅ Function.Injective.orderedCommMonoid | |
| ❌ List.sum_hom <- ✅ List.prod_hom | |
| ❌ AddSubmonoid.subsingleton_iff <- ✅ Submonoid.subsingleton_iff | |
| ❌ AddCon.lift_coe <- ✅ Con.lift_coe | |
| ❌ Set.neg_subset_neg <- ✅ Set.inv_subset_inv | |
| ❌ Set.interᵢ_add_subset <- ✅ Set.interᵢ_mul_subset | |
| ❌ AddCon.lift_apply_mk' <- ✅ Con.lift_apply_mk' | |
| ❌ Set.addCommSemigroup <- ✅ Set.commSemigroup | |
| ❌ Set.add_nonempty <- ✅ Set.mul_nonempty | |
| ❌ WithBot.coe_zero <- ✅ WithBot.coe_one | |
| ❌ Multiset.sum_erase <- ✅ Multiset.prod_erase | |
| ❌ WithTop.zero_eq_coe <- ✅ WithTop.one_eq_coe | |
| ❌ LatticeOrderedCommGroup.abs_abs_sub_abs_le <- ✅ LatticeOrderedCommGroup.abs_abs_div_abs_le | |
| ❌ AddCon.Quotient.inhabited <- ✅ Con.Quotient.inhabited | |
| ❌ Set.add_subset_add_left <- ✅ Set.mul_subset_mul_left | |
| ❌ AddSubmonoid.closure_induction <- ✅ Submonoid.closure_induction | |
| ❌ add_pos_iff <- ✅ one_lt_mul_iff | |
| ❌ AddMonoid.toAddAction <- ✅ Monoid.toMulAction | |
| ❌ Set.unionᵢ₂_vadd <- ✅ Set.unionᵢ₂_smul | |
| ❌ Part.some_sub_some <- ✅ Part.some_div_some | |
| ❌ OrderedAddCommGroup.to_covariantClass_left_le <- ✅ OrderedCommGroup.to_covariantClass_left_le | |
| ❌ add_inf <- ✅ mul_inf | |
| ❌ AddSubmonoid.coe_copy <- ✅ Submonoid.coe_copy | |
| ❌ AddCommute.map <- ✅ Commute.map | |
| ❌ Left.pow_nonneg <- ✅ Left.one_le_pow_of_le | |
| ❌ OrderedAddCommGroup.to_contravariantClass_right_le <- ✅ OrderedCommGroup.to_contravariantClass_right_le | |
| ❌ AddLeftCancelMonoid.toAddMonoid_injective <- ✅ LeftCancelMonoid.toMonoid_injective | |
| ❌ add_neg_nonpos_iff_le <- ✅ mul_inv_le_one_iff_le | |
| ❌ Set.nonempty_neg <- ✅ Set.nonempty_inv | |
| ❌ add_csupᵢ_le <- ✅ mul_csupᵢ_le | |
| ❌ Con.instPowQuotientToMulToMulOneClassNat -> ✅ AddCon.Quotient.nsmul | |
| ❌ Set.add_interᵢ_subset <- ✅ Set.mul_interᵢ_subset | |
| ❌ Set.Nonempty.of_vadd_left <- ✅ Set.Nonempty.of_smul_left | |
| ❌ le_map_add_map_sub <- ✅ le_map_mul_map_div | |
| ❌ AddCon.mk'_ker <- ✅ Con.mk'_ker | |
| ❌ AddCon.hasNeg <- ✅ Con.hasInv | |
| ❌ Set.neg_subset <- ✅ Set.inv_subset | |
| ❌ min_add_add_right <- ✅ min_mul_mul_right | |
| ❌ Set.neg_univ <- ✅ Set.inv_univ | |
| ❌ Set.zero_mem_sub_iff <- ✅ Set.one_mem_div_iff | |
| ❌ Set.vadd_set_eq_empty <- ✅ Set.smul_set_eq_empty | |
| ❌ Set.preimage_add_left_singleton <- ✅ Set.preimage_mul_left_singleton | |
| ❌ AddMonoidHom.map_zsmul' <- ✅ MonoidHom.map_zpow' | |
| ❌ Set.vadd_singleton <- ✅ Set.smul_singleton | |
| ❌ Multiset.sum_le_sum_map <- ✅ Multiset.prod_le_prod_map | |
| ❌ LatticeOrderedCommGroup.neg_le_neg <- ✅ LatticeOrderedCommGroup.inv_le_neg | |
| ❌ Function.Injective.linearOrderedAddCommGroup <- ✅ Function.Injective.linearOrderedCommGroup | |
| ❌ Set.vadd_subset_vadd <- ✅ Set.smul_subset_smul | |
| ❌ nsmul_pos_iff <- ✅ one_lt_pow_iff | |
| ❌ Set.neg_singleton <- ✅ Set.inv_singleton | |
| ❌ nonpos_iff_eq_zero <- ✅ le_one_iff_eq_one | |
| ❌ ite_vadd <- ✅ ite_smul | |
| ❌ Set.sub_subset_iff <- ✅ Set.div_subset_iff | |
| ❌ neg_nonneg_of_nonpos <- ✅ one_le_inv_of_le_one | |
| ❌ add_vadd_comm <- ✅ mul_smul_comm | |
| ❌ Set.preimage_add_right_zero' <- ✅ Set.preimage_mul_right_one' | |
| ❌ sub_neg <- ✅ div_lt_one' | |
| ❌ AddOpposite.unop_injective <- ✅ MulOpposite.unop_injective | |
| ❌ AddSubmonoid.closure_union <- ✅ Submonoid.closure_union | |
| ❌ AddCon.lift_range <- ✅ Con.lift_range | |
| ❌ Set.addActionSet <- ✅ Set.mulActionSet | |
| ❌ AddSubsemigroup.equivMapOfInjective <- ✅ Subsemigroup.equivMapOfInjective | |
| ❌ LatticeOrderedCommGroup.pos_of_nonpos <- ✅ LatticeOrderedCommGroup.pos_of_le_one | |
| ❌ Set.neg_insert <- ✅ Set.inv_insert | |
| ❌ AddSubmonoid.gi <- ✅ Submonoid.gi | |
| ❌ Multiset.sum_map_sum_map <- ✅ Multiset.prod_map_prod_map | |
| ❌ instVAddLex' <- ✅ instSMulLex' | |
| ❌ Set.univ_add_of_zero_mem <- ✅ Set.univ_mul_of_one_mem | |
| ❌ Set.nsmul_subset_nsmul <- ✅ Set.pow_subset_pow | |
| ❌ Set.image_sub <- ✅ Set.image_div | |
| ❌ VAddAssocClass.op_left <- ✅ IsScalarTower.op_left | |
| ❌ AddCon.quotientQuotientEquivQuotient <- ✅ Con.quotientQuotientEquivQuotient | |
| ❌ AddMonoidHom.ext_iff₂ <- ✅ MonoidHom.ext_iff₂ | |
| ❌ Set.sub <- ✅ Set.div | |
| ❌ AddSubmonoid.mem_infₛ <- ✅ Submonoid.mem_infₛ | |
| ❌ AddCon.map_apply <- ✅ Con.map_apply | |
| ❌ neg_lt_sub_iff_lt_add <- ✅ inv_lt_div_iff_lt_mul | |
| ❌ smul_nonpos_iff <- ✅ pow_le_one_iff | |
| ❌ Set.add_empty <- ✅ Set.mul_empty | |
| ❌ WithZero.neg <- ✅ WithOne.inv | |
| ❌ sub_le_sub_flip <- ✅ div_le_div_flip | |
| ❌ Set.vadd_subset_vadd_right <- ✅ Set.smul_subset_smul_right | |
| ❌ AddCon.kerLift_injective <- ✅ Con.kerLift_injective | |
| ❌ FreeAddMonoid.vadd_def <- ✅ FreeMonoid.smul_def | |
| ❌ AddSubsemigroup.supᵢ_induction' <- ✅ Subsemigroup.supᵢ_induction' | |
| ❌ Set.neg_mem_Icc_iff <- ✅ Set.inv_mem_Icc_iff | |
| ❌ Set.unionᵢ_vadd_set <- ✅ Set.unionᵢ_smul_set | |
| ❌ Set.unionᵢ₂_add <- ✅ Set.unionᵢ₂_mul | |
| ❌ Set.vadd_mem_vadd_set_iff <- ✅ Set.smul_mem_smul_set_iff | |
| ❌ Part.right_dom_of_add_dom <- ✅ Part.right_dom_of_mul_dom | |
| ❌ AddCon.addAction <- ✅ Con.mulAction | |
| ❌ le_self_add <- ✅ le_self_mul | |
| ❌ Set.mem_vadd_set_iff_neg_vadd_mem <- ✅ Set.mem_smul_set_iff_inv_smul_mem | |
| ❌ FreeAddMonoid.lift_apply <- ✅ FreeMonoid.lift_apply | |
| ❌ Multiset.le_sum_of_subadditive_on_pred <- ✅ Multiset.le_prod_of_submultiplicative_on_pred | |
| ❌ neg_le_neg <- ✅ inv_le_inv' | |
| ❌ List.Sublist.sum_le_sum <- ✅ List.Sublist.prod_le_prod' | |
| ❌ AddSubmonoid.coe_infₛ <- ✅ Submonoid.coe_infₛ | |
| ❌ AddMonoidHom.map_multiset_sum <- ✅ MonoidHom.map_multiset_prod | |
| ❌ vadd_eq_add <- ✅ smul_eq_mul | |
| ❌ IsAddGroupHom.map_neg <- ✅ IsGroupHom.map_inv | |
| ❌ LinearOrderedAddCommGroup.to_noMaxOrder <- ✅ LinearOrderedCommGroup.to_noMaxOrder | |
| ❌ Part.sub_mem_sub <- ✅ Part.div_mem_div | |
| ❌ AddSubmonoid.closure_induction₂ <- ✅ Submonoid.closure_induction₂ | |
| ❌ neg_lt_sub_iff_lt_add' <- ✅ inv_lt_div_iff_lt_mul' | |
| ❌ vadd_eq_iff_eq_neg_vadd <- ✅ smul_eq_iff_eq_inv_smul | |
| ❌ ZeroHom.withTopMap <- ✅ OneHom.withTopMap | |
| ❌ cmp_sub_zero <- ✅ cmp_div_one' | |
| ❌ IsAddGroupHom.add <- ✅ IsGroupHom.mul | |
| ❌ AddUnits.val_lt_val <- ✅ Units.val_lt_val | |
| ❌ OrderEmbedding.addLeft <- ✅ OrderEmbedding.mulLeft | |
| ❌ Right.neg_lt_self <- ✅ Right.inv_lt_self | |
| ❌ sub_le_sub_iff_left <- ✅ div_le_div_iff_left | |
| ❌ Left.neg_lt_self <- ✅ Left.inv_lt_self | |
| ❌ List.sum_hom₂ <- ✅ List.prod_hom₂ | |
| ❌ sub_le_iff_le_add <- ✅ div_le_iff_le_mul | |
| ❌ le_of_forall_pos_sub_le <- ✅ le_of_forall_one_lt_div_le | |
| ❌ Set.add <- ✅ Set.mul | |
| ❌ Multiset.le_sum_of_subadditive <- ✅ Multiset.le_prod_of_submultiplicative | |
| ❌ AddCancelCommMonoid.ext <- ✅ CancelCommMonoid.ext | |
| ❌ Set.add_univ_of_zero_mem <- ✅ Set.mul_univ_of_one_mem | |
| ❌ AddAction.toFun <- ✅ MulAction.toFun | |
| ❌ Set.pairwiseDisjoint_vadd_iff <- ✅ Set.pairwiseDisjoint_smul_iff | |
| ❌ zero_le <- ✅ one_le | |
| ❌ LatticeOrderedCommGroup.abs_add_le <- ✅ LatticeOrderedCommGroup.mabs_mul_le | |
| ❌ Set.vaddCommClass_set'' <- ✅ Set.smulCommClass_set'' | |
| ❌ Set.Nonempty.of_vadd_right <- ✅ Set.Nonempty.of_smul_right | |
| ❌ FreeAddMonoid.map_comp <- ✅ FreeMonoid.map_comp | |
| ❌ LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice <- ✅ LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice | |
| ❌ Set.vadd_set_Union <- ✅ Set.smul_set_Union | |
| ❌ AddSubmonoid.coe_set_mk <- ✅ Submonoid.coe_set_mk | |
| ❌ AddMonoidHom.flip <- ✅ MonoidHom.flip | |
| ❌ AddCon.lift <- ✅ Con.lift | |
| ❌ Set.empty_vadd <- ✅ Set.empty_smul | |
| ❌ AddSubmonoid.mem_inf <- ✅ Submonoid.mem_inf | |
| ❌ AddSubmonoid.disjoint_def' <- ✅ Submonoid.disjoint_def' | |
| ❌ Set.unionᵢ_neg <- ✅ Set.unionᵢ_inv | |
| ❌ LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub <- ✅ LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div | |
| ❌ FreeAddMonoid.ofList_comp_toList <- ✅ FreeMonoid.ofList_comp_toList | |
| ❌ LatticeOrderedCommGroup.abs_inf_sub_inf_le_abs <- ✅ LatticeOrderedCommGroup.mabs_inf_div_inf_le_mabs | |
| ❌ Set.vadd_unionᵢ₂ <- ✅ Set.smul_unionᵢ₂ | |
| ❌ Left.nonneg_neg_iff <- ✅ Left.one_le_inv_iff | |
| ❌ List.sum_drop_succ <- ✅ List.prod_drop_succ | |
| ❌ AddSubmonoid.closure_induction' <- ✅ Submonoid.closure_induction' | |
| ❌ LatticeOrderedCommGroup.pos_inf_neg_eq_zero <- ✅ LatticeOrderedCommGroup.pos_inf_neg_eq_one | |
| ❌ Set.add_interᵢ₂_subset <- ✅ Set.mul_interᵢ₂_subset | |
| ❌ le_iff_exists_add <- ✅ le_iff_exists_mul | |
| ❌ Option.vadd_none <- ✅ Option.smul_none | |
| ❌ AddAction.exists_vadd_eq <- ✅ MulAction.exists_smul_eq | |
| ❌ Multiset.coe_sum <- ✅ Multiset.coe_prod | |
| ❌ AddMonoidHom.compr₂_apply <- ✅ MonoidHom.compr₂_apply | |
| ❌ Multiset.sum_pair <- ✅ Multiset.prod_pair | |
| ❌ AddEquiv.coe_toAddHom <- ✅ MulEquiv.coe_toMulHom | |
| ❌ Set.isAddUnit_iff_singleton <- ✅ Set.isUnit_iff_singleton | |
| ❌ Set.neg_preimage <- ✅ Set.inv_preimage | |
| ❌ List.sum_cons <- ✅ List.prod_cons | |
| ❌ Multiset.sum_eq_zero <- ✅ Multiset.prod_eq_one | |
| ❌ neg_le_sub_iff_le_add <- ✅ inv_le_div_iff_le_mul | |
| ❌ Fintype.decidableEqAddMonoidHomFintype <- ✅ Fintype.decidableEqMonoidHomFintype | |
| ❌ AddMonoidHom.flip_apply <- ✅ MonoidHom.flip_apply | |
| ❌ lt_neg_iff_add_neg <- ✅ lt_inv_iff_mul_lt_one | |
| ❌ AddSubmonoid.disjoint_def <- ✅ Submonoid.disjoint_def | |
| ❌ min_neg_neg <- ✅ min_inv_inv' | |
| ❌ lt_neg_add_iff_add_lt <- ✅ lt_inv_mul_iff_mul_lt | |
| ❌ Set.sub_interᵢ_subset <- ✅ Set.div_interᵢ_subset | |
| ❌ Set.image_neg <- ✅ Set.image_inv | |
| ❌ LatticeOrderedCommGroup.le_abs <- ✅ LatticeOrderedCommGroup.le_mabs | |
| ❌ Multiset.le_sum_nonempty_of_subadditive <- ✅ Multiset.le_prod_nonempty_of_submultiplicative | |
| ❌ AddSubmonoid.subset_closure <- ✅ Submonoid.subset_closure | |
| ❌ Set.zero_mem_zero <- ✅ Set.one_mem_one | |
| ❌ zero_vadd_eq_id <- ✅ one_smul_eq_id | |
| ❌ Set.vaddSet <- ✅ Set.smulSet | |
| ❌ FreeAddMonoid.map_of <- ✅ FreeMonoid.map_of | |
| ❌ AddCon.map <- ✅ Con.map | |
| ❌ AddRightCancelSemigroup.toIsRightCancelAdd <- ✅ RightCancelSemigroup.toIsRightCancelMul | |
| ❌ add_neg_le_neg_add_iff <- ✅ mul_inv_le_inv_mul_iff | |
| ❌ Function.extend_vadd <- ✅ Function.extend_smul | |
| ❌ Part.sub_get_eq <- ✅ Part.div_get_eq | |
| ❌ Antitone.neg <- ✅ Antitone.inv | |
| ❌ AddSubmonoid.Simps.coe <- ✅ Submonoid.Simps.coe | |
| ❌ add_neg_lt_neg_add_iff <- ✅ mul_inv_lt_inv_mul_iff | |
| ❌ Set.singleton_add <- ✅ Set.singleton_mul | |
| ❌ List.sum_add_sum_eq_sum_zipWith_add_sum_drop <- ✅ List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop | |
| ❌ Set.vadd_set_symm_diff <- ✅ Set.smul_set_symm_diff | |
| ❌ AddCon.mrange_mk' <- ✅ Con.mrange_mk' | |
| ❌ Left.pow_nonpos <- ✅ Left.pow_le_one_of_le | |
| ❌ LatticeOrderedCommGroup.neg_part_def <- ✅ LatticeOrderedCommGroup.m_neg_part_def | |
| ❌ List.sum_replicate <- ✅ List.prod_replicate | |
| ❌ Set.add_union <- ✅ Set.mul_union | |
| ❌ neg_add_le_iff_le_add <- ✅ inv_mul_le_iff_le_mul | |
| ❌ Multiset.sum_le_card_nsmul <- ✅ Multiset.prod_le_pow_card | |
| ❌ AddMonoidHom.eqLocusM <- ✅ MonoidHom.eqLocusM | |
| ❌ AddSubmonoid.mem_infᵢ <- ✅ Submonoid.mem_infᵢ | |
| ❌ Set.subset_zero_iff_eq <- ✅ Set.subset_one_iff_eq | |
| ❌ List.sum_le_card_nsmul <- ✅ List.prod_le_pow_card | |
| ❌ Multiset.single_le_sum <- ✅ Multiset.single_le_prod | |
| ❌ AddAction.injective <- ✅ MulAction.injective | |
| ❌ FreeAddMonoid.ofList_map <- ✅ FreeMonoid.ofList_map | |
| ❌ Set.Nonempty.of_add_right <- ✅ Set.Nonempty.of_mul_right | |
| ❌ AddEquiv.withZeroCongr_refl <- ✅ MulEquiv.withOneCongr_refl | |
| ❌ AddCon.hasSub <- ✅ Con.hasDiv | |
| ❌ LatticeOrderedCommGroup.pos_eq_zero_iff <- ✅ LatticeOrderedCommGroup.pos_eq_one_iff | |
| ❌ Set.image_op_add <- ✅ Set.image_op_mul | |
| ❌ FreeAddMonoid.map <- ✅ FreeMonoid.map | |
| ❌ Set.add_subset_add <- ✅ Set.mul_subset_mul | |
| ❌ neg_lt_neg_iff <- ✅ inv_lt_inv_iff | |
| ❌ List.sum_pos <- ✅ List.one_lt_prod_of_one_lt | |
| ❌ Sigma.vadd_def <- ✅ Sigma.smul_def | |
| ❌ FreeAddMonoid.toList_zero <- ✅ FreeMonoid.toList_one | |
| ❌ List.single_le_sum <- ✅ List.single_le_prod | |
| ❌ Set.unionᵢ_neg_vadd <- ✅ Set.unionᵢ_inv_smul | |
| ❌ le_sub_comm <- ✅ le_div_comm | |
| ❌ FreeAddMonoid.recOn_zero <- ✅ FreeMonoid.recOn_one | |
| ❌ Multiset.sum_hom₂ <- ✅ Multiset.prod_hom₂ | |
| ❌ exists_zero_lt <- ✅ exists_one_lt' | |
| ❌ inf_add_sup <- ✅ inf_mul_sup | |
| ❌ IsAddUnit.set <- ✅ IsUnit.set | |
| ❌ instVAddLex <- ✅ instSMulLex | |
| ❌ LatticeOrderedCommGroup.pos_sub_neg <- ✅ LatticeOrderedCommGroup.pos_div_neg | |
| ❌ LatticeOrderedCommGroup.neg_eq_pos_neg <- ✅ LatticeOrderedCommGroup.neg_eq_pos_inv | |
| ❌ FreeAddMonoid.toList_comp_ofList <- ✅ FreeMonoid.toList_comp_ofList | |
| ❌ LatticeOrderedCommGroup.neg_nonpos_iff <- ✅ LatticeOrderedCommGroup.neg_le_one_iff | |
| ❌ AddCon.induction_on_addUnits <- ✅ Con.induction_on_units | |
| ❌ List.sum_hom_rel <- ✅ List.prod_hom_rel | |
| ❌ le_neg_add_iff_le <- ✅ le_inv_mul_iff_le | |
| ❌ Multiset.sum_eq_foldr <- ✅ Multiset.prod_eq_foldr | |
| ❌ Set.subset_add_left <- ✅ Set.subset_mul_left | |
| ❌ List.length_pos_of_sum_neg <- ✅ List.length_pos_of_prod_lt_one | |
| ❌ AddAction.compHom <- ✅ MulAction.compHom | |
| ❌ FreeAddMonoid.casesOn_of_add <- ✅ FreeMonoid.casesOn_of_mul | |
| ❌ AddCon.addSemigroup <- ✅ Con.semigroup | |
| ❌ le_iff_forall_pos_le_add <- ✅ le_iff_forall_one_lt_le_mul | |
| ❌ AddCon.mk' <- ✅ Con.mk' | |
| ❌ List.alternatingSum_cons <- ✅ List.alternatingProd_cons | |
| ❌ le_of_forall_pos_lt_add <- ✅ le_of_forall_one_lt_lt_mul | |
| ❌ AddAction.Regular.isPretransitive <- ✅ MulAction.Regular.isPretransitive | |
| ❌ Function.const_neg <- ✅ Function.const_lt_one | |
| ❌ AddLeftCancelMonoid.ext <- ✅ LeftCancelMonoid.ext | |
| ❌ eq_zero_of_neg_eq <- ✅ eq_one_of_inv_eq' | |
| ❌ Multiset.sum_map_zero <- ✅ Multiset.prod_map_one | |
| ❌ Set.add_mem_add <- ✅ Set.mul_mem_mul | |
| ❌ AddSubmonoid.closure_le <- ✅ Submonoid.closure_le | |
| ❌ LatticeOrderedCommGroup.neg_of_nonpos <- ✅ LatticeOrderedCommGroup.neg_of_le_one | |
| ❌ Left.pow_neg <- ✅ Left.pow_lt_one_of_lt | |
| ❌ Set.singletonAddMonoidHom <- ✅ Set.singletonMonoidHom | |
| ❌ AddUnits.val_mkOfAddEqZero <- ✅ Units.val_mkOfMulEqOne | |
| ❌ List.sum_map_add <- ✅ List.prod_map_mul | |
| ❌ AddOpposite.unop_sub <- ✅ MulOpposite.unop_div | |
| ❌ csupᵢ_add_csupᵢ_le <- ✅ csupᵢ_mul_csupᵢ_le | |
| ❌ MulOpposite.op_inv -> ✅ AddOpposite.op_neg | |
| ❌ AddCon.kerLift <- ✅ Con.kerLift | |
| ❌ AddMonoidHom.eqLocusM_same <- ✅ MonoidHom.eqLocusM_same | |
| ❌ le_sub_iff_add_le <- ✅ le_div_iff_mul_le | |
| ❌ Set.mem_add <- ✅ Set.mem_mul | |
| ❌ Set.neg_mem_Ico_iff <- ✅ Set.inv_mem_Ico_iff | |
| ❌ Set.singleton_zero <- ✅ Set.singleton_one | |
| ❌ Set.singleton_add_singleton <- ✅ Set.singleton_mul_singleton | |
| ❌ List.Perm.sum_eq' <- ✅ List.Perm.prod_eq' | |
| ❌ List.alternatingSum_reverse <- ✅ List.alternatingProd_reverse | |
| ❌ SubNegMonoid.ext <- ✅ DivInvMonoid.ext | |
| ❌ FreeAddMonoid.hom_eq <- ✅ FreeMonoid.hom_eq | |
| ❌ AddMonoidHom.eq_of_eqOn_topM <- ✅ MonoidHom.eq_of_eqOn_topM | |
| ❌ Multiset.sum_eq_foldl <- ✅ Multiset.prod_eq_foldl | |
| ❌ Set.preimage_add_left_zero' <- ✅ Set.preimage_mul_left_one' | |
| ❌ Pi.Lex.orderedAddCommGroup <- ✅ Pi.Lex.orderedCommGroup | |
| ❌ vadd_left_cancel_iff <- ✅ smul_left_cancel_iff | |
| ❌ Set.interᵢ₂_sub_subset <- ✅ Set.interᵢ₂_div_subset | |
| ❌ Multiset.sum_map_neg <- ✅ Multiset.prod_map_inv | |
| ❌ Set.set_vadd_subset_iff <- ✅ Set.set_smul_subset_iff | |
| ❌ List.alternatingSum_singleton <- ✅ List.alternatingProd_singleton | |
| ❌ neg_le_iff_add_nonneg <- ✅ inv_le_iff_one_le_mul | |
| ❌ WithTop.map_zero <- ✅ WithTop.map_one | |
| ❌ WithTop.top_ne_zero <- ✅ WithTop.top_ne_one | |
| ❌ List.sum_map_erase <- ✅ List.prod_map_erase | |
| ❌ Set.vadd_mem_vadd_set <- ✅ Set.smul_mem_smul_set | |
| ❌ LatticeOrderedCommGroup.Birkhoff_inequalities <- ✅ LatticeOrderedCommGroup.m_Birkhoff_inequalities | |
| ❌ Set.vadd_set_unionᵢ₂ <- ✅ Set.smul_set_unionᵢ₂ | |
| ❌ Set.vadd_set_subset_iff <- ✅ Set.smul_set_subset_iff | |
| ❌ AddGroup.toSubNegAddMonoid_injective <- ✅ Group.toDivInvMonoid_injective | |
| ❌ AddAction.surjective <- ✅ MulAction.surjective | |
| ❌ le_map_add_map_sub <- ✅ le_map_add_map_div | |
| ❌ bot_eq_zero <- ✅ bot_eq_one | |
| ❌ le_add_cinfᵢ <- ✅ le_mul_cinfᵢ | |
| ❌ LatticeOrderedCommGroup.pos_abs <- ✅ LatticeOrderedCommGroup.m_pos_abs | |
| ❌ max_sub_sub_right <- ✅ max_div_div_right' | |
| ❌ Left.neg_pos_iff <- ✅ Left.one_lt_inv_iff | |
| ❌ StrictAntiOn.neg <- ✅ StrictAntiOn.inv | |
| ❌ AddSemiconjBy.transitive <- ✅ SemiconjBy.transitive | |
| ❌ Option.vadd_def <- ✅ Option.smul_def | |
| ❌ Set.Nonempty.of_add_left <- ✅ Set.Nonempty.of_mul_left | |
| ❌ Set.interᵢ_sub_subset <- ✅ Set.interᵢ_div_subset | |
| ❌ List.sum_neg <- ✅ List.prod_inv | |
| ❌ Function.Surjective.addActionLeft <- ✅ Function.Surjective.mulActionLeft | |
| ❌ Multiset.sum_hom' <- ✅ Multiset.prod_hom' | |
| ❌ WithTop.zero <- ✅ WithTop.one | |
| ❌ eq_neg_vadd_iff <- ✅ eq_inv_smul_iff | |
| ❌ AddSubsemigroup.coe_supᵢ_of_directed <- ✅ Subsemigroup.coe_supᵢ_of_directed | |
| ❌ Set.add_unionᵢ <- ✅ Set.mul_unionᵢ | |
| ❌ sub_lt_iff_lt_add <- ✅ div_lt_iff_lt_mul | |
| ❌ AddMonoidHom.compl₂_apply <- ✅ MonoidHom.compl₂_apply | |
| ❌ vadd_pi_subset <- ✅ smul_pi_subset | |
| ❌ Set.mem_neg <- ✅ Set.mem_inv | |
| ❌ Set.sub_nonempty <- ✅ Set.div_nonempty | |
| ❌ pos_iff_ne_zero <- ✅ one_lt_iff_ne_one | |
| ❌ lt_iff_exists_add <- ✅ lt_iff_exists_mul | |
| ❌ AddCon.zsmul <- ✅ Con.zpow |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment