Documentation Verification Report

VerySmallDoubling

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

Statistics

Metric	Count
Definitions `instFintypeSubtypeMemSubgroupInvMulSubgroup`, `invMulSubgroup`	2
Theorems `card_inv_mul_of_doubling_lt_three_halves`, `card_mul_finset_lt_two`, `doubling_lt_golden_ratio`, `doubling_lt_three_halves`, `doubling_lt_two`, `invMulSubgroup_eq_inv_mul`, `invMulSubgroup_eq_mul_inv`, `mul_inv_eq_inv_mul_of_doubling_lt_two`, `op_smul_stabilizer_of_no_doubling`, `op_vadd_stabilizer_of_no_doubling`, `smul_inv_mul_eq_inv_mul_opSMul`, `smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves`, `smul_stabilizer_of_no_doubling`, `vadd_stabilizer_of_no_doubling`	14
Total	16

Finset

Definitions

Name	Category	Theorems
`instFintypeSubtypeMemSubgroupInvMulSubgroup` 📖	CompOp	—
`invMulSubgroup` 📖	CompOp	2 math math: `invMulSubgroup_eq_mul_inv`, `invMulSubgroup_eq_inv_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_inv_mul_of_doubling_lt_three_halves` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves` `card_smul_finset`
`card_mul_finset_lt_two` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne` `Nonempty` `card` `Real.instNatCast` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instMul` `Real.instSub` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	`Fintype.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `Set.mul`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `LT.lt.le` `card_pos` `LT.lt.trans_le` `Nonempty.card_pos` `sub_le_sub` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Nat.mono_cast` `Real.instZeroLEOneClass` `le_of_not_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_overlap_pf` `CancelDenoms.mul_subst` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Set.toFinset_card` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Nat.cast_pos'` `NeZero.one` `one_ne_zero` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `One.instNonempty` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `Nat.cast_mul` `Set.toFinset_mul` `toFinset_coe` `Fintype.subsingleton` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `sub_mul` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `le_imp_le_of_le_of_le` `add_le_add_right` `le_refl` `card_le_card` `Subgroup.one_mem` `sub_sub_cancel` `Fintype.card_pos` `Nat.cast_nonneg'` `Set.subset_mul_right`
`doubling_lt_golden_ratio` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.goldenRatio` `Real.instLE` `Real.instNatCast` `card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Real.instMul`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.goldenConj` `Set` `Set.mul` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `instSetLike`	—	`lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Tactic.Linarith.add_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Real.goldenConj_neg` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Real.goldenRatio_lt_two` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_pos` `eq_empty_or_nonempty` `CharP.cast_eq_zero` `CharP.ofCharZero` `coe_empty` `Set.mul_empty` `le_of_lt` `MulAction.stabilizer_coe_finset` `MulAction.stabilizer_finite` `finite_toSet` `nonempty_fintype` `MulAction.stabilizer_mul_self` `coe_mul` `Set.coe_toFinset` `convolution_inv` `convolution.congr_simp` `inv_inv` `card_inv` `card_product` `Nat.cast_mul` `card_eq_sum_card_fiberwise` `mul_mem_mul` `mem_product` `sum_congr` `filter.congr_simp` `sum_filter_add_sum_filter_not` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `sum_le_sum` `Nat.mono_cast` `Real.instZeroLEOneClass` `convolution_le_card_left` `sum_const` `nsmul_eq_mul` `card_filter_add_card_filter_not` `Nat.cast_add` `add_sub_cancel_left` `mul_assoc` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Nonempty.card_pos` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_mul_le_mul_right` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_pos'` `NeZero.one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `div_mul_eq_mul_div` `Real.goldenRatio_mul_goldenConj` `Real.goldenRatio_add_goldenConj` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `one_ne_zero` `GroupWithZero.toNontrivial` `card_le_card` `MulAction.mem_stabilizer_finset'` `card_mul_inv_eq_convolution_inv` `inter_subset_inter` `inter_subset_right` `union_subset` `inter_subset_left` `card_inter_add_card_union` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `neg_eq_zero` `CancelDenoms.add_subst` `sub_eq_zero_of_eq` `card_smul_inter_smul` `Set.toFinset_card` `inv_div` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `One.instNonempty` `inv_anti₀` `IsUnit.mul_div_cancel_right`
`doubling_lt_three_halves` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Fintype.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op`	—	`Fintype.card_congr'` `Nat.card_eq_finsetCard` `card_inv_mul_of_doubling_lt_three_halves` `invMulSubgroup_eq_inv_mul` `instIsConcreteLE` `smul_inv_mul_eq_inv_mul_opSMul`
`doubling_lt_two` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne` `Nonempty` `Real.instNatCast` `card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Real.instMul` `Real.instSub` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	`Fintype.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `Set.mul`	—	`Nat.instAtLeastTwoHAddOfNat` `card_mul_finset_lt_two` `le_refl`
`invMulSubgroup_eq_inv_mul` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`SetLike.coe` `Subgroup` `Subgroup.instSetLike` `invMulSubgroup` `Set` `Set.mul` `instSetLike` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`invMulSubgroup_eq_mul_inv` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`SetLike.coe` `Subgroup` `Subgroup.instSetLike` `invMulSubgroup` `Set` `Set.mul` `instSetLike` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`invMulSubgroup_eq_inv_mul` `mul_inv_eq_inv_mul_of_doubling_lt_two` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_mul` `Int.cast_natCast` `Int.cast_mul` `Int.cast_ofNat` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Rat.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Mathlib.Tactic.Linarith.mul_neg` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_nonpos`
`mul_inv_eq_inv_mul_of_doubling_lt_two` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Subset.antisymm` `inv_inv` `card_inv`
`op_smul_stabilizer_of_no_doubling` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instMembership`	`MulOpposite` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulOpposite.instMonoid` `MulAction.toSemigroupAction` `Monoid.toOppositeMulAction` `MulOpposite.op` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulAction.stabilizer` `mulActionFinset` `Monoid.toMulAction` `instSetLike`	—	—
`op_vadd_stabilizer_of_no_doubling` 📖	mathematical	`card` `Finset` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instMembership`	`HVAdd.hVAdd` `AddOpposite` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddOpposite.instAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toOppositeAddAction` `AddOpposite.op` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddAction.stabilizer` `addActionFinset` `AddMonoid.toAddAction` `instSetLike`	—	—
`smul_inv_mul_eq_inv_mul_opSMul` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instMembership`	`smulFinset` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op`	—	`subset_antisymm` `instAntisymmSubset` `subset_smul_finset_iff` `MulOpposite.op_inv` `instIsTransSubset` `op_smul_finset_subset_mul` `inv_inv` `Mathlib.Tactic.GCongr.rel_imp_rel` `mul_subset_mul` `smul_finset_subset_mul` `subset_refl` `instReflSubset` `coe_mul` `mul_assoc` `invMulSubgroup_eq_mul_inv` `coe_mul_coe` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `invMulSubgroup_eq_inv_mul` `mul_inv_eq_inv_mul_of_doubling_lt_two`
`smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instMembership`	`smulFinset` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `MulOpposite` `MulOpposite.instMonoid` `Monoid.toOppositeMulAction` `MulOpposite.op` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset`
`smul_stabilizer_of_no_doubling` 📖	mathematical	`card` `Finset` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instMembership`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulAction.stabilizer` `mulActionFinset` `instSetLike`	—	—
`vadd_stabilizer_of_no_doubling` 📖	mathematical	`card` `Finset` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instMembership`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddAction.stabilizer` `addActionFinset` `instSetLike`	—	—

---

← Back to Index