| Name | Category | Theorems |
|---|
commGroupWithZero 📖 | CompOp | — |
commRing 📖 | CompOp | 90 mathmath: NumberField.basisMatrix_eq_embeddingsMatrixReindex, AdjoinRoot.instNumberFieldRat, NumberField.norm_norm_le_norm_mul_house_pow, Polynomial.sum_bernoulli, CongruenceSubgroup.exists_Gamma_le_conj', NumberField.mixedEmbedding.norm_eq_norm, NumberField.FinitePlace.prod_eq_inv_abs_norm, NNRat.mk_zero, StarAddMonoid.toStarModuleRat, NumberField.Units.dirichletUnitTheorem.seq_next, CongruenceSubgroup.exists_Gamma_le_conj, NNRat.coe_indicator, IsCyclotomicExtension.Rat.discr_prime_pow', Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, Algebra.coe_norm_int, NumberField.det_basisOfFractionalIdeal_eq_absNorm, Matrix.num_zero, NumberField.Units.norm, LieDerivation.exp_map_apply, CongruenceSubgroup.IsArithmetic.conj, Matrix.den_zero, NNRat.mk_natCast, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, LieDerivation.exp_apply, CongruenceSubgroup.isArithmetic_conj_SL2Z, instPosMulMono, wittStructureRat_prop, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast, wittStructureRat_rec, AddSubgroup.relIndex_eq_abs_det, cast_det, Polynomial.bernoulli_eq_sub_sum, RootPairing.instIsValuedInRatOfIsCrystallographic, wittStructureRat_rec_aux, FractionalIdeal.absNorm_span_singleton, CongruenceSubgroup.finiteIndex_conjGL, DivisibleHull.qsmul_def, cast_list_sum, instSubsingletonLieAlgebraRat, xInTermsOfW_vars_subset, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, Matrix.num_natCast, LieAlgebra.toModule_injective, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, bernsteinPolynomial.linearIndependent_aux, Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, instCharZero, Polynomial.cyclotomic_eq_minpoly_rat, Polynomial.bernoulli_def, Matrix.den_intCast, RootPairing.pairingIn_rat, uniformSpace_eq, NumberField.Embeddings.coeff_bdd_of_norm_le, cosetToCuspOrbit_apply_mk, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, Matrix.num_one, Padic.coe_withValRingEquiv, WittVector.map_frobeniusPoly, instIsTopologicalRing, instTrivialStar, isDomain, Padic.coe_withValRingEquiv_symm, FractionalIdeal.abs_det_basis_change, xInTermsOfW_vars_aux, Matrix.num_intCast, NumberField.isAlgebraic, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, DivisibleHull.instIsStrictOrderedModuleRat, Complex.isIntegral_rat_I, instStarOrderedRing, Matrix.num_eq_zero_iff, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Matrix.den_one, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, MonoidWithZeroHomClass.ext_rat_iff, IsCyclotomicExtension.Rat.discr_odd_prime', NumberField.coe_discr, bernsteinPolynomial.linearIndependent, NumberField.InfinitePlace.prod_eq_abs_norm, map_wittStructureInt, Algebra.coe_trace_int, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, Matrix.den_natCast, Subgroup.IsArithmetic.conj, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', LinearOrderedField.toPosSMulStrictMono_rat
|
commSemiring 📖 | CompOp | 116 mathmath: NumberField.basisMatrix_eq_embeddingsMatrixReindex, DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul, NumberField.InfinitePlace.sum_mult_eq, NumberField.integralBasis_apply, instSMulCommClass, NumberField.canonicalEmbedding.latticeBasis_apply, HurwitzZeta.cosZeta_two_mul_nat', NumberField.norm_norm_le_norm_mul_house_pow, AlgHom.toRingHom_toRatAlgHom, Polynomial.sum_bernoulli, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, HurwitzZeta.cosZeta_two_mul_nat, NumberField.abs_discr_ge', NumberField.adjoin_eq_top_of_infinitePlace_lt, RingHom.map_rat_algebraMap, RingHom.toRatAlgHom_apply, NumberField.IsTotallyComplex.finrank, NumberField.IsTotallyReal.finrank, Polynomial.bernoulli_generating_function, RingHom.toRatAlgHom_toRingHom, Matrix.inv_denom_smul_num, wittStructureRat_vars, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, NumberField.canonicalEmbedding.integralBasis_repr_apply, HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.Units.finrank_mul_regOfFamily_eq_det, HurwitzZeta.hurwitzZeta_neg_nat, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, RingEquivClass.toLinearEquivClassRat, instSMulCommClass', NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.Embeddings.card, PowerSeries.exp_pow_sum, hasSum_one_div_nat_pow_mul_cos, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, NumberField.to_finiteDimensional, wittStructureRat_prop, Polynomial.cyclotomic.isCoprime_rat, wittStructureRat_rec, RingHomClass.toLinearMapClassRat, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, PowerSeries.coeff_exp, NumberField.RingOfIntegers.rank, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, NumberField.integralBasis_repr_apply, wittStructureRat_rec_aux, DivisionRing.continuousConstSMul_rat, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, NumberField.mixedEmbedding.norm_smul, HurwitzZeta.sinZeta_two_mul_nat_add_one', IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, Subfield.bot_eq_of_charZero, isFractionRing, isEmpty_algebraRat_iff_mixedCharZero, RingHom.equivRatAlgHom_apply, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, NumberField.finite_of_discr_bdd, NormedSpace.exp_def, EqualCharZero.nonempty_algebraRat_iff, Real.rank_rat_real, HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, NumberField.inverse_basisMatrix_mulVec_eq_repr, isLocalizationIsInteger_iff, HurwitzZeta.sinZeta_two_mul_nat_add_one, NumberField.Embeddings.coeff_bdd_of_norm_le, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, NumberField.exists_ideal_in_class_of_norm_le, constantCoeff_wittStructureRat_zero, NumberField.mem_span_integralBasis, NumberField.mem_span_basisOfFractionalIdeal, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, NumberField.mixedEmbedding.logMap_apply, NumberField.mixedEmbedding.latticeBasis_apply, hasSum_one_div_nat_pow_mul_sin, NumberField.abs_discr_ge_of_isTotallyComplex, NumberField.mixedEmbedding.latticeBasis_repr_apply, WittVector.map_frobeniusPoly, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsCyclotomicExtension.Rat.finrank, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, FractionalIdeal.abs_det_basis_change, NumberField.mixedEmbedding.norm_real, Complex.rank_rat_complex, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, NumberField.abs_discr_rpow_ge_of_isTotallyComplex, NumberField.basisOfFractionalIdeal_apply, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.euclidean.finrank, instIsLocalizationIntPosRat, NormedSpace.exp_eq_tsum_rat, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.coe_discr, NumberField.Units.finrank_mul_regulator_eq_det, map_wittStructureInt, NumberField.mixedEmbedding.convexBodySum_volume, algebra_rat_subsingleton, NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd, Polynomial.Gal.splits_ℚ_ℂ, NumberField.house.basis_repr_norm_le_const_mul_house, RingHom.equivRatAlgHom_symm_apply, NNRat.instContinuousSMulRatReal, Complex.nonempty_linearEquiv_real, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal
|
semiring 📖 | CompOp | 152 mathmath: padicNorm.instIsAbsoluteValueRat, NumberField.basisMatrix_eq_embeddingsMatrixReindex, Module.End.exp_mul_of_derivation, Polynomial.bernoulli_eval_one_sub, DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul, NumberField.InfinitePlace.sum_mult_eq, NumberField.integralBasis_apply, fermatLastTheoremFor_iff_rat, NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.norm_norm_le_norm_mul_house_pow, Polynomial.sum_bernoulli, Padic.complete', Polynomial.bernoulli_eval_one, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, padicNormE.nonarchimedean', NumberField.abs_discr_ge', FractionalIdeal.absNorm_eq', NNRat.floor_coe, padicNormE.image', Polynomial.bernoulli_succ_eval, AddMonoidHom.toRatLinearMap_injective, StarAddMonoid.toStarModuleRat, Polynomial.bernoulli_eval_zero, NumberField.IsTotallyComplex.finrank, CategoryTheory.Functor.ratLinear, NumberField.IsTotallyReal.finrank, Polynomial.bernoulli_generating_function, CongruenceSubgroup.exists_Gamma_le_conj, Polynomial.bernoulli_eval_one_add, padicNormE.eq_padic_norm', coe_castHom, IsNilpotent.exp_smul_eq_sum, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, NumberField.canonicalEmbedding.integralBasis_repr_apply, castHom_rat, subsingleton_rat_module, NumberField.Units.finrank_mul_regOfFamily_eq_det, AbsoluteValue.exists_nat_rpow_iff_isEquiv, NumberField.det_basisOfFractionalIdeal_eq_absNorm, Polynomial.sum_range_pow_eq_bernoulli_sub, AbsoluteValue.equiv_on_nat_iff_equiv, padicNormE.defn, subsingleton_ringHom, FractionalIdeal.absNorm_bot, padicNormE.add_eq_max_of_ne', LieDerivation.exp_map_apply, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, RingEquivClass.toLinearEquivClassRat, Polynomial.bernoulli_zero, Polynomial.bernoulli_eval_neg, LieDerivation.exp_apply, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.Embeddings.card, Padic.padicNormE.is_norm, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, AbsoluteValue.padic_eq_padicNorm, Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast, RingHomClass.toLinearMapClassRat, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, IsScalarTower.rat, natFloor_natCast_div_natCast, Polynomial.bernoulli_eq_sub_sum, NumberField.RingOfIntegers.rank, NumberField.integralBasis_repr_apply, FractionalIdeal.absNorm_eq, NumberField.mixedEmbedding.norm_smul, Module.End.commute_exp_left_of_commute, Polynomial.bernoulli_comp_one_add_X, Padic.complete'', SMulCommClass.rat', FractionalIdeal.absNorm_span_singleton, AddMonoidHom.coe_toRatLinearMap, fermatLastTheoremWith_nat_int_rat_tfae, star_qsmul, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, NNRat.ceil_coe, Algebra.TensorProduct.instCompatibleSMulRat, bernsteinPolynomial.linearIndependent_aux, Padic.exi_rat_seq_conv, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, Real.rank_rat_real, NumberField.inverse_basisMatrix_mulVec_eq_repr, Polynomial.bernoulli_def, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, AbsoluteValue.padic_le_one, NumberField.Embeddings.coeff_bdd_of_norm_le, hahnEmbedding_isOrderedModule_rat, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, NumberField.exists_ideal_in_class_of_norm_le, ringOfIntegersEquiv_apply_coe, FractionalIdeal.absNorm_nonneg, NumberField.mem_span_integralBasis, IsNilpotent.exp_eq_sum, NumberField.mem_span_basisOfFractionalIdeal, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, NumberField.mixedEmbedding.logMap_apply, Polynomial.X_pow_sub_X_sub_one_irreducible_rat, NumberField.mixedEmbedding.latticeBasis_apply, Padic.isUniformInducing_cast_withVal, AbsoluteValue.not_real_equiv_padic, instIsStrictOrderedRing, NumberField.abs_discr_ge_of_isTotallyComplex, NumberField.mixedEmbedding.latticeBasis_repr_apply, Padic.rat_dense', IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsCyclotomicExtension.Rat.finrank, AbsoluteValue.eq_on_nat_iff_eq, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Padic.coe_withValRingEquiv_symm, FractionalIdeal.abs_det_basis_change, AbsoluteValue.real_eq_abs, Polynomial.derivative_bernoulli_add_one, AbsoluteValue.not_real_isEquiv_padic, Polynomial.bernoulli_one, NumberField.mixedEmbedding.norm_real, Complex.rank_rat_complex, NumberField.abs_discr_rpow_ge_of_isTotallyComplex, NumberField.basisOfFractionalIdeal_apply, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, Matrix.conjTranspose_rat_smul, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.euclidean.finrank, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Polynomial.coeff_bernoulli, Polynomial.derivative_bernoulli, MonoidWithZeroHomClass.ext_rat_iff, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.coe_discr, map_rat_smul, bernsteinPolynomial.linearIndependent, NumberField.Units.finrank_mul_regulator_eq_det, FractionalIdeal.coeIdeal_absNorm, NumberField.mixedEmbedding.convexBodySum_volume, Polynomial.bernoulli_comp_one_sub_X, NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd, FractionalIdeal.absNorm_eq_zero_iff, Polynomial.bernoulli_comp_neg_X, Polynomial.bernoulli_three_eval_one_quarter, AbsoluteValue.apply_le_sum_digits, star_rat_smul, Padic.isDenseInducing_cast_withVal, NumberField.house.basis_repr_norm_le_const_mul_house, SMulCommClass.rat, Complex.nonempty_linearEquiv_real, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, FractionalIdeal.absNorm_one, NNRat.coe_coeHom
|