| Name | Category | Theorems |
|---|
smul 📖 | CompOp | 47 mathmath: smul_mem_smul, Nonempty.zero_smul, image_smul_product, isScalarTower'', smul_finset_subset_smul, card_dvd_card_smul_right, isScalarTower', smul_singleton, smulCommClass_finset'', smul_univ, Set.toFinset_smul, smul_neg, singleton_smul, smul_subset_smul_right, smul_union, inter_smul_union_subset_union, Nonempty.smul, smul_nonempty_iff, union_smul, smul_subset_smul, Set.Finite.toFinset_smul, Fintype.piFinset_smul, op_smul_finset_smul_eq_smul_smul_finset, smul_univ₀', smulCommClass, smul_def, inter_smul_subset, smul_empty, mem_smul, card_smul_le, smul_inter_subset, subset_smul, biUnion_smul_finset, smul_subset_iff, zero_smul_subset, zero_mem_smul_iff, coe_smul, smul_zero_subset, Nonempty.smul_zero, neg_smul, smul_subset_smul_left, union_smul_inter_subset_union, smul_univ₀, smulCommClass_finset', singleton_smul_singleton, empty_smul, smul_eq_empty
|
smulFinset 📖 | CompOp | 94 mathmath: isScalarTower, smul_finset_subset_smul_finset_iff, smul_finset_sdiff, mul_subset_iff_right, inv_smul_mem_iff, op_smul_finset_mul_eq_mul_smul_finset, inv_smul_finset_distrib, smul_finset_subset_smul, image_smul_distrib, smul_finset_inter, smul_finset_univ, subset_smul_finset_iff, op_smul_finset_subset_mul, inv_op_smul_finset_distrib, smul_finset_subset_smul_finset_iff₀, zero_mem_smul_finset_iff, mulDysonETransform_snd, smul_mem_smul_finset_iff, smul_mem_smul_finset_iff₀, singleton_mul, smul_inv_mul_eq_inv_mul_opSMul, smul_finset_symmDiff, smul_finset_univ₀, isScalarTower', mul_mem_smul_finset_iff, mem_inv_smul_finset_iff, smul_finset_singleton, smulCommClass_finset, smulCommClass_finset'', pairwiseDisjoint_smul_iff, smul_finset_inter_subset, smul_finset_subset_iff₀, singleton_smul, smul_finset_symmDiff₀, image_smul_comm, Set.Finite.toFinset_smul_set, smul_finset_nonempty, smul_finset_subset_iff, inv_smul_finset_distrib₀, coe_smul_finset, smul_finset_subset_smul_finset, isCentralScalar, smul_finset_neg, card_smul_inter, smul_finset_empty, mulDysonETransform_fst, mulDysonETransform.smul_finset_snd_subset_fst, Nonempty.smul_finset, image_smul, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, mul_subset_iff_left, op_smul_finset_smul_eq_smul_smul_finset, inv_op_smul_finset_distrib₀, smul_finset_union, smul_mem_smul_finset, smul_finset_def, smul_finset_eq_univ, op_smul_convolution_eq_convolution_smul, smul_finset_card_le, smul_finset_eq_empty, Equiv.Perm.cycleFactorsFinset_conj_eq, Fintype.piFinset_smul_finset, smul_convolution_eq_convolution_inv_mul, neg_smul_finset, mem_smul_finset, card_inter_smul, smul_finset_insert, mulETransformRight_fst, zero_smul_finset, card_smul_inter_smul, dens_smul_finset, inv_smul_mem_iff₀, mulETransformRight_snd, mem_inv_smul_finset_iff₀, subset_smul_finset_iff₀, smul_finset_inter₀, smul_finset_sdiff₀, biUnion_op_smul_finset, biUnion_smul_finset, Set.toFinset_smul_set, zero_smul_finset_subset, card_smul_finset, mulETransformLeft_snd, smulCommClass_finset', mulETransformLeft_fst, mul_singleton, Set.powersetCard.coe_smul, smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves, MulAction.mem_stabilizer_finset_iff_subset_smul_finset, zero_mem_smul_finset, nsmul_piAntidiag_univ, smul_finset_subset_mul, convolution_op_smul_eq_convolution_mul_inv, nsmul_piAntidiag
|
vadd 📖 | CompOp | 38 mathmath: vadd_nonempty_iff, vaddAssocClass'', vadd_eq_empty, vadd_mem_vadd, Fintype.piFinset_vadd, vadd_empty, card_vadd_le, inter_vadd_subset, mem_vadd, vadd_subset_iff, union_vadd_inter_subset_union, vadd_inter_subset, vadd_union, singleton_vadd_singleton, Nonempty.vadd, vaddCommClass_finset'', coe_vadd, subset_vadd, biUnion_vadd_finset, vadd_subset_vadd_right, op_vadd_finset_vadd_eq_vadd_vadd_finset, vadd_univ, vadd_finset_subset_vadd, Set.toFinset_vadd, vaddAssocClass', Set.Finite.toFinset_vadd, inter_vadd_union_subset_union, vadd_singleton, vadd_subset_vadd, vaddCommClass_finset', empty_vadd, vadd_def, union_vadd, vadd_subset_vadd_left, image_vadd_product, singleton_vadd, card_dvd_card_vadd_right, vaddCommClass
|
vaddFinset 📖 | CompOp | 72 mathmath: Fintype.piFinset_vadd_finset, isCentralVAdd, image_vadd_comm, vadd_finset_eq_univ, neg_op_vadd_finset_distrib, coe_vadd_finset, vadd_finset_singleton, add_singleton, vadd_finset_univ, vadd_addConvolution_eq_addConvolution_neg_add, image_vadd_distrib, card_vadd_finset, op_vadd_finset_subset_add, vaddAssocClass, vadd_finset_symmDiff, vadd_finset_inter, Set.toFinset_vadd_set, addDysonETransform_snd, vadd_finset_subset_iff, vadd_finset_nonempty, Set.Finite.toFinset_vadd_set, vadd_finset_def, add_subset_iff_right, mem_vadd_finset, vaddCommClass_finset'', add_mem_vadd_finset_iff, vadd_finset_subsetSum_subset_subsetSum_insert, card_inter_vadd, addDysonETransform_fst, biUnion_op_vadd_finset, vadd_finset_card_le, mem_neg_vadd_finset_iff, op_vadd_finset_add_eq_add_vadd_finset, add_subset_iff_left, singleton_add, image_vadd, vadd_finset_union, vadd_finset_insert, vaddCommClass_finset, op_vadd_addConvolution_eq_addConvolution_vadd, vadd_finset_empty, vadd_finset_subset_add, biUnion_vadd_finset, pairwiseDisjoint_vadd_iff, AddAction.mem_stabilizer_finset_iff_subset_vadd_finset, vadd_finset_inter_subset, addETransformRight_snd, addETransformLeft_snd, op_vadd_finset_vadd_eq_vadd_vadd_finset, addDysonETransform.vadd_finset_snd_subset_fst, vadd_finset_eq_empty, addETransformLeft_fst, vadd_finset_subset_vadd, vaddAssocClass', Nonempty.vadd_finset, vadd_mem_vadd_finset_iff, card_vadd_inter, neg_vadd_mem_iff, vadd_finset_subset_vadd_finset_iff, subset_vadd_finset_iff, vadd_mem_vadd_finset, addConvolution_op_vadd_eq_addConvolution_add_neg, vaddCommClass_finset', vadd_finset_subset_vadd_finset, vadd_finset_sdiff, addETransformRight_fst, card_vadd_inter_vadd, dens_vadd_finset, neg_vadd_finset_distrib, singleton_vadd, Set.powersetCard.coe_vadd, AddAction.mem_stabilizer_finset_iff_vadd_finset_subset
|
vsub 📖 | CompOp | 25 mathmath: Set.Finite.toFinset_vsub, empty_vsub, vsub_subset_vsub_left, singleton_vsub_singleton, vsub_mem_vsub, image_vsub_product, vsub_subset_vsub, vsub_subset_iff, Set.toFinset_vsub, inter_vsub_subset, vsub_eq_empty, vsub_empty, union_vsub, vsub_nonempty, vsub_union, mem_vsub, Nonempty.vsub, singleton_vsub, vsub_card_le, vsub_subset_vsub_right, subset_vsub, coe_vsub, vsub_singleton, vsub_def, vsub_inter_subset
|