DoublingConst

📁 Source: Mathlib/Combinatorics/Additive/DoublingConst.lean

Statistics

Metric	Count
Definitions «termδ[_,_]», «termδ[_]», «termδₘ[_,_]», «termδₘ[_]», «termσ[_,_]», «termσ[_]», «termσₘ[_,_]», «termσₘ[_]», addConst, divConst, mulConst, subConst	12
Theorems addConst_empty_left, addConst_empty_right, addConst_le_card, addConst_le_inv_dens, addConst_le_subConst_sq, addConst_mul_card, addConst_neg_left, addConst_neg_right, card_mul_addConst, card_mul_cast_addConst, card_mul_cast_divConst, card_mul_cast_mulConst, card_mul_cast_subConst, card_mul_divConst, card_mul_mulConst, card_mul_subConst, cast_addConst, cast_addConst_mul_card, cast_divConst, cast_divConst_mul_card, cast_mulConst, cast_mulConst_mul_card, cast_subConst, cast_subConst_mul_card, divConst_empty_left, divConst_empty_right, divConst_inv_left, divConst_inv_right, divConst_le_card, divConst_le_inv_dens, divConst_le_mulConst_sq, divConst_mul_card, mulConst_empty_left, mulConst_empty_right, mulConst_inv_left, mulConst_inv_right, mulConst_le_card, mulConst_le_divConst_sq, mulConst_le_inv_dens, mulConst_mul_card, nonneg_addConst, nonneg_addConst_self, nonneg_subConst, nonneg_subConst_self, one_le_divConst, one_le_divConst_self, one_le_mulConst, one_le_mulConst_self, subConst_empty_left, subConst_empty_right, subConst_le_addConst_sq, subConst_le_card, subConst_le_inv_dens, subConst_mul_card, subConst_neg_left, subConst_neg_right	56
Total	68

Combinatorics.Additive

Definitions

Name	Category	Theorems
«termδ[_,_]» 📖	CompOp	—
«termδ[_]» 📖	CompOp	—
«termδₘ[_,_]» 📖	CompOp	—
«termδₘ[_]» 📖	CompOp	—
«termσ[_,_]» 📖	CompOp	—
«termσ[_]» 📖	CompOp	—
«termσₘ[_,_]» 📖	CompOp	—
«termσₘ[_]» 📖	CompOp	—

Finset

Definitions

Name	Category	Theorems
addConst 📖	CompOp	17 math math: card_mul_cast_addConst, addConst_le_inv_dens, subConst_le_addConst_sq, addConst_neg_right, card_mul_addConst, subConst_neg_left, addConst_le_subConst_sq, subConst_neg_right, nonneg_addConst, addConst_le_card, nonneg_addConst_self, addConst_mul_card, addConst_neg_left, cast_addConst_mul_card, addConst_empty_left, addConst_empty_right, cast_addConst
divConst 📖	CompOp	17 math math: card_mul_divConst, divConst_mul_card, divConst_le_card, divConst_le_mulConst_sq, mulConst_inv_left, one_le_divConst, divConst_empty_left, one_le_divConst_self, divConst_inv_right, mulConst_inv_right, cast_divConst_mul_card, cast_divConst, divConst_inv_left, divConst_empty_right, divConst_le_inv_dens, card_mul_cast_divConst, mulConst_le_divConst_sq
mulConst 📖	CompOp	17 math math: mulConst_mul_card, one_le_mulConst_self, mulConst_le_card, one_le_mulConst, divConst_le_mulConst_sq, card_mul_mulConst, mulConst_inv_left, mulConst_empty_left, cast_mulConst_mul_card, mulConst_le_inv_dens, cast_mulConst, card_mul_cast_mulConst, divConst_inv_right, mulConst_inv_right, mulConst_empty_right, divConst_inv_left, mulConst_le_divConst_sq
subConst 📖	CompOp	17 math math: card_mul_subConst, subConst_le_addConst_sq, addConst_neg_right, cast_subConst_mul_card, subConst_neg_left, addConst_le_subConst_sq, subConst_neg_right, card_mul_cast_subConst, cast_subConst, subConst_le_card, subConst_mul_card, addConst_neg_left, nonneg_subConst_self, subConst_empty_right, subConst_le_inv_dens, subConst_empty_left, nonneg_subConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addConst_empty_left 📖	mathematical	—	addConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	empty_add Nat.cast_zero div_zero
addConst_empty_right 📖	mathematical	—	addConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	add_empty Nat.cast_zero zero_div
addConst_le_card 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat addConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card	—	eq_empty_or_nonempty addConst_empty_left zero_le NNRat.instCanonicallyOrderedAdd addConst.eq_1 div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos Nat.cast_mul Nat.cast_le card_add_le
addConst_le_inv_dens 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat addConst NNRat.instInv dens	—	dens.eq_1 inv_div addConst.eq_1 div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass card_le_univ Nat.cast_nonneg'
addConst_le_subConst_sq 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat addConst AddCommGroup.toAddGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield subConst	—	eq_empty_or_nonempty addConst_empty_right subConst_empty_right zero_pow Nat.instAtLeastTwoHAddOfNat OfNat.ofNat_ne_zero Nat.instCharZero NNRat.nonpos_iff_eq_zero le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat mul_assoc addConst_mul_card Nat.cast_mul Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_add_sub_sub subConst_mul_card Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
addConst_mul_card 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield addConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	eq_empty_or_nonempty Nat.cast_zero MulZeroClass.mul_zero empty_add div_mul_cancel₀ ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos
addConst_neg_left 📖	mathematical	—	addConst AddCommGroup.toAddGroup Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid subConst	—	addConst.eq_1 subConst.eq_1 card_neg neg_add_rev neg_neg neg_add_eq_sub
addConst_neg_right 📖	mathematical	—	addConst Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid subConst	—	addConst.eq_1 subConst.eq_1 sub_eq_add_neg
card_mul_addConst 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card addConst Finset add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mul_comm addConst_mul_card
card_mul_cast_addConst 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card NNRat.cast DivisionSemiring.toNNRatCast addConst Finset add AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	NNRat.cast_natCast card_mul_addConst
card_mul_cast_divConst 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card NNRat.cast DivisionSemiring.toNNRatCast divConst Finset div DivInvMonoid.toDiv Group.toDivInvMonoid	—	NNRat.cast_natCast card_mul_divConst
card_mul_cast_mulConst 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card NNRat.cast DivisionSemiring.toNNRatCast mulConst Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	NNRat.cast_natCast card_mul_mulConst
card_mul_cast_subConst 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card NNRat.cast DivisionSemiring.toNNRatCast subConst Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	NNRat.cast_natCast card_mul_subConst
card_mul_divConst 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card divConst Finset div DivInvMonoid.toDiv Group.toDivInvMonoid	—	mul_comm divConst_mul_card
card_mul_mulConst 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card mulConst Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul_comm mulConst_mul_card
card_mul_subConst 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card subConst Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	mul_comm subConst_mul_card
cast_addConst 📖	mathematical	—	NNRat.cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring addConst DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring card Finset add AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	NNRat.cast_div NNRat.cast_natCast
cast_addConst_mul_card 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast addConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset add AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	NNRat.cast_natCast addConst_mul_card
cast_divConst 📖	mathematical	—	NNRat.cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring divConst DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring card Finset div Group.toDivInvMonoid	—	NNRat.cast_div NNRat.cast_natCast
cast_divConst_mul_card 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast divConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid	—	NNRat.cast_natCast divConst_mul_card
cast_mulConst 📖	mathematical	—	NNRat.cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring mulConst DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	NNRat.cast_div NNRat.cast_natCast
cast_mulConst_mul_card 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast mulConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	NNRat.cast_natCast mulConst_mul_card
cast_subConst 📖	mathematical	—	NNRat.cast DivisionSemiring.toNNRatCast Semifield.toDivisionSemiring subConst DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	NNRat.cast_div NNRat.cast_natCast
cast_subConst_mul_card 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast subConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	NNRat.cast_natCast subConst_mul_card
divConst_empty_left 📖	mathematical	—	divConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	empty_div Nat.cast_zero div_zero
divConst_empty_right 📖	mathematical	—	divConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	div_empty Nat.cast_zero zero_div
divConst_inv_left 📖	mathematical	—	divConst CommGroup.toGroup Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid mulConst	—	mulConst.eq_1 divConst.eq_1 card_inv inv_div div_inv_eq_mul mul_comm
divConst_inv_right 📖	mathematical	—	divConst Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid mulConst	—	mulConst.eq_1 divConst.eq_1 div_inv_eq_mul
divConst_le_card 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat divConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card	—	eq_empty_or_nonempty divConst_empty_left NNRat.instCanonicallyOrderedAdd divConst.eq_1 div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos card_div_le
divConst_le_inv_dens 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat divConst NNRat.instInv dens	—	dens.eq_1 inv_div divConst.eq_1 div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass card_le_univ Nat.cast_nonneg'
divConst_le_mulConst_sq 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat divConst Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield mulConst	—	eq_empty_or_nonempty divConst_empty_right mulConst_empty_right zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat mul_assoc divConst_mul_card IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_div_mul_mul mulConst_mul_card Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
divConst_mul_card 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield divConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset div DivInvMonoid.toDiv Group.toDivInvMonoid	—	eq_empty_or_nonempty Nat.cast_zero MulZeroClass.mul_zero empty_div div_mul_cancel₀ ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos
mulConst_empty_left 📖	mathematical	—	mulConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	empty_mul Nat.cast_zero div_zero
mulConst_empty_right 📖	mathematical	—	mulConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	mul_empty Nat.cast_zero zero_div
mulConst_inv_left 📖	mathematical	—	mulConst CommGroup.toGroup Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid divConst	—	mulConst.eq_1 divConst.eq_1 card_inv mul_inv_rev inv_inv inv_mul_eq_div
mulConst_inv_right 📖	mathematical	—	mulConst Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid divConst	—	mulConst.eq_1 divConst.eq_1 div_eq_mul_inv
mulConst_le_card 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat mulConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card	—	eq_empty_or_nonempty mulConst_empty_left NNRat.instCanonicallyOrderedAdd mulConst.eq_1 div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos card_mul_le
mulConst_le_divConst_sq 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat mulConst CommGroup.toGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield divConst	—	eq_empty_or_nonempty mulConst_empty_right divConst_empty_right zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat mul_assoc mulConst_mul_card IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_mul_div_div divConst_mul_card Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
mulConst_le_inv_dens 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat mulConst NNRat.instInv dens	—	dens.eq_1 inv_div mulConst.eq_1 div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass card_le_univ Nat.cast_nonneg'
mulConst_mul_card 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield mulConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	eq_empty_or_nonempty Nat.cast_zero MulZeroClass.mul_zero empty_mul div_mul_cancel₀ ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos
nonneg_addConst 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield addConst	—	addConst.eq_1 one_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing NNRat.instNontrivial card_pos Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero card_le_card_add_right AddRightCancelSemigroup.toIsRightCancelAdd
nonneg_addConst_self 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield addConst	—	nonneg_addConst
nonneg_subConst 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield subConst	—	addConst_neg_right nonneg_addConst neg_nonempty_iff
nonneg_subConst_self 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield subConst	—	nonneg_subConst
one_le_divConst 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield divConst	—	mulConst_inv_right one_le_mulConst
one_le_divConst_self 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield divConst	—	one_le_divConst
one_le_mulConst 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield mulConst	—	mulConst.eq_1 one_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat IsStrictOrderedRing.toIsOrderedRing NNRat.instNontrivial IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero card_le_card_mul_right RightCancelSemigroup.toIsRightCancelMul
one_le_mulConst_self 📖	mathematical	Nonempty	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield mulConst	—	one_le_mulConst
subConst_empty_left 📖	mathematical	—	subConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	empty_sub Nat.cast_zero div_zero
subConst_empty_right 📖	mathematical	—	subConst Finset instEmptyCollection NNRat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	sub_empty Nat.cast_zero zero_div
subConst_le_addConst_sq 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat subConst Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield addConst	—	eq_empty_or_nonempty subConst_empty_right addConst_empty_right zero_pow Nat.instAtLeastTwoHAddOfNat OfNat.ofNat_ne_zero Nat.instCharZero NNRat.nonpos_iff_eq_zero le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat mul_assoc subConst_mul_card Nat.cast_mul Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero ruzsa_triangle_inequality_sub_add_add addConst_mul_card Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' NeZero.charZero_one Nonempty.card_pos
subConst_le_card 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat subConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield card	—	eq_empty_or_nonempty subConst_empty_left zero_le NNRat.instCanonicallyOrderedAdd subConst.eq_1 div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos Nat.cast_mul Nat.cast_le card_sub_le
subConst_le_inv_dens 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat subConst NNRat.instInv dens	—	dens.eq_1 inv_div subConst.eq_1 div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass card_le_univ Nat.cast_nonneg'
subConst_mul_card 📖	mathematical	—	NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield subConst AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	eq_empty_or_nonempty Nat.cast_zero MulZeroClass.mul_zero empty_sub div_mul_cancel₀ ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one NNRat.instCharZero Nonempty.card_pos
subConst_neg_left 📖	mathematical	—	subConst AddCommGroup.toAddGroup Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid addConst	—	addConst.eq_1 subConst.eq_1 card_neg neg_sub sub_neg_eq_add add_comm
subConst_neg_right 📖	mathematical	—	subConst Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid addConst	—	addConst.eq_1 subConst.eq_1 sub_neg_eq_add

---

← Back to Index