| Name | Category | Theorems |
|---|
addCommGroup 📖 | CompOp | 9 mathmath: CharacterModule.int.divByNat_self, CharacterModule.smul_apply, CharacterModule.instLinearMapClassIntAddCircleRatOfNat, CharacterModule.curry_apply_apply, CharacterModule.ext_iff, CharacterModule.homEquiv_symm_apply_apply_apply, CharacterModule.uncurry_apply, CharacterModule.homEquiv_apply_apply, CharacterModule.dual_apply
|
addCommMonoid 📖 | CompOp | 33 mathmath: cast_finsupp_sum, Polynomial.bernoulli_succ_eval, NNRat.toNNRat_sum_of_nonneg, Matrix.map_mul_ratCast, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, Polynomial.sum_range_pow_eq_bernoulli_sub, AhlswedeZhang.IsAntichain.le_infSum, bernoulli_spec', bernoulli'_spec, instIsOrderedAddMonoid, bernoulli'_spec', sum_Ico_pow, padicValRat.sum_pos_of_pos, AhlswedeZhang.infSum_compls_add_supSum, sum_bernoulli', Subgroup.one_le_sum_inv_index_of_leftCoset_cover, padicNorm.sum_lt, AhlswedeZhang.supSum_of_univ_notMem, cast_sum, AddSubgroup.one_le_sum_inv_index_of_leftCoset_cover, padicValRat.lt_sum_of_lt, harmonic_eq_sum_Icc, AhlswedeZhang.supSum_singleton, sum_range_pow, instArchimedeanRat, bernoulli'_def, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, cast_multiset_sum, bernoulli'_def', sum_bernoulli, padicNorm.sum_le, padicNorm.sum_le', padicNorm.sum_lt'
|
addCommSemigroup 📖 | CompOp | — |
addGroup 📖 | CompOp | 75 mathmath: Real.ofCauchy_sup, NNRat.abs_coe, NumberField.mixedEmbedding.norm_eq_norm, coe_nnabs, NumberField.FinitePlace.prod_eq_inv_abs_norm, Real.ofCauchy_zero, NumberField.Units.dirichletUnitTheorem.seq_next, Real.of_near, Real.ofCauchy_mul, Real.cauchy_sub, Real.mk_one, num_abs_eq_abs_num, Real.ofCauchy_nnratCast, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, Real.lt_cauchy, finite_rat_abs_sub_lt_one_div_den_sq, NumberField.det_basisOfFractionalIdeal_eq_absNorm, Real.ofCauchy_sub, Real.mk_lt, NumberField.Units.norm, SimpleGraph.nonuniformWitnesses_spec, Real.mk_mul, Real.cauchy_inv, Real.cauchy_nnratCast, Real.mk_add, AddSubgroup.relIndex_eq_abs_det, SimpleGraph.not_isUniform_iff, uniformContinuous_abs, Real.ofCauchy_natCast, Real.cauchy_natCast, FractionalIdeal.absNorm_span_singleton, Real.ofCauchy_ratCast, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, den_abs_eq_den, Real.ofCauchy_intCast, Real.ofCauchy_div, cast_abs, abs_def, Real.cauchy_neg, Real.mk_const, Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul, Real.cauchy_intCast, Real.mk_zero, Real.cauchy_add, Real.ofCauchy_add, Real.ofCauchy_inv, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, Real.cauchy_zero, Real.ofCauchy_neg, SimpleGraph.nonuniformWitness_spec, infinitePlace_apply, Real.mk_inf, Real.mk_eq, instIsUniformAddGroup, Real.ofCauchy_one, NumberField.isUnit_iff_norm, FractionalIdeal.abs_det_basis_change, AbsoluteValue.real_eq_abs, Real.mk_sup, sqrt_eq, Real.cauchy_one, Real.cauchy_ratCast, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, Real.cauchy_mul, Real.ringEquivCauchy_apply, Real.mk_neg, NumberField.InfinitePlace.prod_eq_abs_norm, instIsTopologicalAddGroup, NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion, Real.mk_le, Real.ringEquivCauchy_symm_apply_cauchy, Real.isCauSeq_iff_lift, abs_def', Real.ofCauchy_inf
|
addLeftCancelSemigroup 📖 | CompOp | — |
addMonoid 📖 | CompOp | 4 mathmath: addSubmonoid_closure_range_pow, RootPairing.linearIndepOn_root_baseOf, addSubmonoid_closure_range_mul_self, NNRat.nsmul_coe
|
addRightCancelSemigroup 📖 | CompOp | — |
addSemigroup 📖 | CompOp | — |
commMonoid 📖 | CompOp | 6 mathmath: Nat.totient_eq_mul_prod_factors, cast_finsuppProd, cast_multiset_prod, NNRat.toNNRat_prod_of_nonneg, commProb_pi, cast_prod
|
commSemigroup 📖 | CompOp | — |
divCasesOn 📖 | CompOp | — |
monoid 📖 | CompOp | 17 mathmath: Nat.ratSqrt_sq_le, StarAddMonoid.toStarModuleRat, IsNilpotent.exp_smul_eq_sum, finite_rat_abs_sub_lt_one_div_den_sq, IsScalarTower.rat, SMulCommClass.rat', star_qsmul, Algebra.TensorProduct.instCompatibleSMulRat, cast_smul_eq_qsmul, IsNilpotent.exp_eq_sum, Nat.lt_ratSqrt_add_inv_prec_sq, Subgroup.commProb_subgroup_le, Matrix.conjTranspose_rat_smul, map_rat_smul, star_rat_smul, commProb_def, SMulCommClass.rat
|
semigroup 📖 | CompOp | — |