Rat

📁 Source: Mathlib/Algebra/Algebra/Rat.lean

Statistics

Metric	Count
Definitions toRatAlgebra, toNNRatAlgebra	2
Theorems instSMulCommClass, instSMulCommClass', algebra_rat_subsingleton, instSMulCommClass, instSMulCommClass', toLinearEquivClassRat, map_rat_algebraMap, toLinearMapClassNNRat, toLinearMapClassRat	9
Total	11

DivisionRing

Definitions

Name	Category	Theorems
toRatAlgebra 📖	CompOp	121 math math: NumberField.basisMatrix_eq_embeddingsMatrixReindex, NumberField.InfinitePlace.sum_mult_eq, NumberField.integralBasis_apply, Rat.instSMulCommClass, NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.IsCMField.unitsComplexConj_torsion, HurwitzZeta.cosZeta_two_mul_nat', NumberField.norm_norm_le_norm_mul_house_pow, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.mixedEmbedding.norm_eq_norm, HurwitzZeta.cosZeta_two_mul_nat, NumberField.FinitePlace.prod_eq_inv_abs_norm, NumberField.abs_discr_ge', NumberField.adjoin_eq_top_of_infinitePlace_lt, IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, NumberField.IsTotallyComplex.finrank, NumberField.Units.dirichletUnitTheorem.seq_next, NumberField.IsTotallyReal.finrank, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, IsCyclotomicExtension.Rat.discr_prime_pow', IsCyclotomicExtension.Rat.absdiscr_prime_pow, NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le, NumberField.canonicalEmbedding.integralBasis_repr_apply, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, IntermediateField.isTotallyReal_bot, Algebra.coe_norm_int, NumberField.Units.finrank_mul_regOfFamily_eq_det, HurwitzZeta.hurwitzZeta_neg_nat, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.Units.norm, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, RingEquivClass.toLinearEquivClassRat, Rat.instSMulCommClass', IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, IsCyclotomicExtension.Rat.discr, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.Embeddings.card, hasSum_one_div_nat_pow_mul_cos, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, NumberField.to_finiteDimensional, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ, RingHomClass.toLinearMapClassRat, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.is_primitive_element_of_infinitePlace_lt, IsCyclotomicExtension.Rat.discr_prime_pow_succ, NumberField.RingOfIntegers.rank, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, NumberField.integralBasis_repr_apply, 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, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, IsCyclotomicExtension.Rat.natAbs_discr, NumberField.finite_of_discr_bdd, NumberField.IsCMField.unitsMulComplexConjInv_apply, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, IsCyclotomicExtension.Rat.absdiscr_prime, Real.rank_rat_real, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, NumberField.inverse_basisMatrix_mulVec_eq_repr, Polynomial.cyclotomic_eq_minpoly_rat, IsCyclotomicExtension.Rat.discr_prime_pow, HurwitzZeta.sinZeta_two_mul_nat_add_one, NumberField.Embeddings.coeff_bdd_of_norm_le, NumberField.exists_ideal_in_class_of_norm_le, 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, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, hasSum_one_div_nat_pow_mul_sin, NumberField.abs_discr_ge_of_isTotallyComplex, NumberField.mixedEmbedding.latticeBasis_repr_apply, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsCyclotomicExtension.Rat.finrank, NumberField.mixedEmbedding.finrank, NumberField.isUnit_iff_norm, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, NumberField.isAlgebraic, 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, Complex.isIntegral_rat_I, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.euclidean.finrank, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, IsCyclotomicExtension.Rat.discr_odd_prime', NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.coe_discr, NumberField.Units.finrank_mul_regulator_eq_det, NumberField.InfinitePlace.prod_eq_abs_norm, IsCyclotomicExtension.Rat.discr_prime, Algebra.coe_trace_int, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, NumberField.mixedEmbedding.convexBodySum_volume, NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd, Polynomial.Gal.splits_ℚ_ℂ, NumberField.IsCMField.complexConj_torsion, NumberField.house.basis_repr_norm_le_const_mul_house, NNRat.instContinuousSMulRatReal, Complex.nonempty_linearEquiv_real, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal

DivisionSemiring

Definitions

Name	Category	Theorems
toNNRatAlgebra 📖	CompOp	41 math math: AddDissociated.randomisation, RCLike.norm_expect_le, Complex.re_balance, Complex.im_expect, NNRat.instSMulCommClass', RCLike.ofReal_balance, Ring.choose_eq_smul, RCLike.ofReal_comp_balance, RCLike.wInner_cWeight_eq_expect, Complex.re_comp_balance, AddChar.expect_apply_eq_zero_iff_ne_zero, Complex.ofReal_balance, binomialSeries_apply, Finset.expect_boole_mul', RCLike.wInner_cWeight_const_left, AddChar.expect_eq_zero_iff_ne_zero, Complex.ofReal_comp_balance, Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, Complex.im_balance, Complex.ofReal_expect, NNRat.instSMulCommClass, Finset.expect_boole_mul, Complex.im_comp_balance, NNReal.coe_expect, RCLike.ofReal_expect, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, RingHomClass.toLinearMapClassNNRat, RCLike.nnnorm_nnqsmul, Complex.re_expect, RCLike.wInner_cWeight_const_right, Finset.expect_div, MeasureTheory.lpNorm_expect_le, Real.compact_inner_le_weight_mul_Lp_of_nonneg, algebraMap.coe_expect, Finset.expect_eq_sum_div_card, AddChar.expect_apply_eq_ite, RCLike.wInner_cWeight_eq_smul_wInner_one, AddChar.expect_eq_ite, Complex.ofReal_choose, RCLike.norm_nnqsmul, Fintype.expect_eq_sum_div_card

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSMulCommClass 📖	mathematical	—	SMulCommClass NNRat Algebra.toSMul instCommSemiringNNRat DivisionSemiring.toSemiring DivisionSemiring.toNNRatAlgebra	—	smul_def mul_smul_comm
instSMulCommClass' 📖	mathematical	—	SMulCommClass NNRat Algebra.toSMul instCommSemiringNNRat DivisionSemiring.toSemiring DivisionSemiring.toNNRatAlgebra	—	SMulCommClass.symm instSMulCommClass

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebra_rat_subsingleton 📖	mathematical	—	Algebra commSemiring	—	Algebra.algebra_ext RingHom.congr_fun subsingleton_ringHom
instSMulCommClass 📖	mathematical	—	SMulCommClass Algebra.toSMul commSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivisionRing.toRatAlgebra	—	smul_def mul_smul_comm
instSMulCommClass' 📖	mathematical	—	SMulCommClass Algebra.toSMul commSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivisionRing.toRatAlgebra	—	SMulCommClass.symm instSMulCommClass

RingEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearEquivClassRat 📖	mathematical	—	LinearEquivClass Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivisionRing.toRatAlgebra	—	RingHomInvPair.ids toAddEquivClass Algebra.smul_def eq_ratCast RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass toNonUnitalRingHomClass map_ratCast toRingHomClass

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_rat_algebraMap 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring instFunLike CommSemiring.toSemiring Rat.commSemiring algebraMap	—	ext_iff Rat.subsingleton_ringHom

RingHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearMapClassNNRat 📖	mathematical	—	LinearMapClass NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra	—	AddMonoidHomClass.toAddHomClass toAddMonoidHomClass NNRat.smul_def map_mul NonUnitalRingHomClass.toMulHomClass toNonUnitalRingHomClass map_nnratCast eq_nnratCast RingHom.instRingHomClass
toLinearMapClassRat 📖	mathematical	—	LinearMapClass Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivisionRing.toRatAlgebra	—	SemilinearMapClass.toAddHomClass toLinearMapClassNNRat Rat.smul_def map_mul NonUnitalRingHomClass.toMulHomClass toNonUnitalRingHomClass map_ratCast eq_ratCast RingHom.instRingHomClass

---

← Back to Index