NatInt

📁 Source: Mathlib/Algebra/Module/NatInt.lean

Statistics

Metric	Count
Definitions toIntModule, uniqueIntModule, toNatModule, uniqueNatModule, addCommMonoidToAddCommGroup, instMulActionIntOfSubtractionMonoid, instMulActionNatOfAddMonoid, instSMulWithZeroInt, instSMulWithZeroNat	9
Theorems intIsScalarTower, nat_isScalarTower, subsingletonIntModule, subsingletonNatModule, of_module, toAddMonoidHom_eq_nsmulAddMonoidHom, toAddMonoidHom_eq_zsmulAddGroupHom, cast_smul_eq_zsmul, smul_one_eq_cast, cast_smul_eq_nsmul, smul_one_eq_cast, int_smul_eq_zsmul, map_intCast_smul, map_natCast_smul, nat_smul_eq_nsmul, ofNat_smul_eq_nsmul	16
Total	25

AddCommGroup

Definitions

Name	Category	Theorems
toIntModule 📖	CompOp	334 math math: NumberField.basisMatrix_eq_embeddingsMatrixReindex, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Module.isTorsionFree_int_iff_isAddTorsionFree, FreeAbelianGroup.instFiniteInt, Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, NumberField.integralBasis_apply, PeriodPair.hasSumLocallyUniformly_weierstrassP, NumberField.Units.logEmbedding_fundSystem, Differential.implicitDeriv_C, PeriodPair.coeff_weierstrassPExceptSeries, Profinite.NobelingProof.injective_πs', Differential.algHom_deriv, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, RootPairing.EmbeddedG2.mem_span_of_mem_allRoots, PeriodPair.derivWeierstrassPExcept_sub, NumberField.Units.fun_eq_repr, NumberField.canonicalEmbedding.latticeBasis_apply, addMonoidHomLequivInt_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, PeriodPair.ω₁_div_two_notMem_lattice, Profinite.NobelingProof.Products.span_nil_eq_top, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, Profinite.NobelingProof.coe_πs, RootPairing.Base.root_mem_span_int, Module.Basis.ofZLatticeBasis_apply, NumberField.mixedEmbedding.mem_idealLattice, BoxIntegral.unitPartition.mem_smul_span_iff, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.weierstrassP_coe, ZSpan.smul, Module.Basis.ofZLatticeComap_apply, instLieModuleInt, Algebra.discr_eq_discr, Profinite.NobelingProof.Products.max_eq_eval, Profinite.NobelingProof.Products.eval_πs, Ring.choose_eq_smul, PeriodPair.hasSum_derivWeierstrassPExcept, LocallyConstant.freeOfProfinite, ZLattice.comap_discreteTopology, CharacterModule.instLinearMapClassIntAddCircleRatOfNat, ModN.basis_apply_eq_mkQ, ZLattice.comap_toAddSubgroup, Profinite.NobelingProof.Products.eval_πs', BoxIntegral.unitPartition.integralSum_eq_tsum_div, ZLattice.module_finite, PeriodPair.latticeBasis_zero, DifferentialAlgebra.deriv_algebraMap, tendsto_card_div_pow_atTop_volume, RootPairing.finrank_corootSpanIn_int, ZLattice.rank, ZSpan.quotientEquiv_apply_mk, PeriodPair.ω₂_div_two_notMem_lattice, PeriodPair.hasSum_derivWeierstrassP, PeriodPair.compl_lattice_diff_singleton_mem_nhds, AddSubgroup.index_eq_natAbs_det, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.succ_exact, RootPairing.Base.coroot_mem_span_int, Submodule.torsion_int, Module.Free.addMonoidHom, Profinite.NobelingProof.GoodProducts.smaller_factorization, ZLattice.covolume.tendsto_card_div_pow, PeriodPair.mem_lattice, instCountable_of_discrete_submodule, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, Profinite.NobelingProof.πs'_apply_apply, RootPairing.finrank_rootSpanIn_int, NumberField.Units.span_basisOfIsMaxRank, NumberField.canonicalEmbedding.integralBasis_repr_apply, Finsupp.toFreeAbelianGroup_comp_singleAddHom, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Submodule.span_int_eq, Module.End.intCast_def, ZSpan.repr_ceil_apply, NonUnitalSubring.unitization_apply, NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers, ZLattice.comap_equiv_apply, CommRingCat.coproductCocone_inl, ZLattice.FG, Module.Basis.addSubgroupOfClosure_repr_apply, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, PeriodPair.isClosed_lattice, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, Real.finrank_eq_int_finrank_of_discrete, NumberField.det_basisOfFractionalIdeal_eq_absNorm, algebraMap.coe_deriv, LieModule.isNilpotent_iff_int, PeriodPair.periodic_derivWeierstrassP, NumberField.RingOfIntegers.instIsNoetherianInt, Differential.coeff_mapCoeffs, Submodule.finiteQuotient_iff, AddSubgroup.toIntSubmodule_symm, NumberField.mixedEmbedding.span_idealLatticeBasis, Polynomial.descPochhammer_smeval_eq_descFactorial, NumberField.Units.fundSystem_mk, CommRingCat.coproductCocone_inr, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, PeriodPair.differentiableOn_derivWeierstrassP, PeriodPair.weierstrassPExcept_def, Representation.norm_ofMulDistribMulAction_eq, NumberField.Units.rank_modTorsion, Module.Basis.ofZLatticeBasis_span, CharacterModule.intSpanEquivQuotAddOrderOf_apply, NumberField.mixedEmbedding.mem_span_latticeBasis, fwdDiff_aux.shiftₗ_pow_apply, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, NumberField.mixedEmbedding.covolume_idealLattice, Submodule.span_singleton_toAddSubgroup_eq_zmultiples, OreLocalization.zsmul_eq_zsmul, Submodule.toIntSubmodule_toAddSubgroup, Profinite.NobelingProof.Products.eval_πs_image', Ring.descPochhammer_smeval_add, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, NumberField.discr_eq_discr, NumberField.Units.regOfFamily_of_isMaxRank, ModN.natCard_eq, RootPairing.IsG2.span_eq_rootSpan_int, ZSpan.coe_floor_self, Differential.mapCoeffs_monomial, ZLattice.module_free, instIsZLatticeRealSpan, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, Differential.mapCoeffs_C, PeriodPair.derivWeierstrassP_sub_coe, Submodule.toAddSubgroup_toIntSubmodule, Profinite.NobelingProof.GoodProducts.span, Submodule.natAbs_det_equiv, NumberField.RingOfIntegers.rank, addMonoidEndRingEquivInt_apply, Submodule.span_int_eq_addSubgroup_closure, NumberField.integralBasis_repr_apply, ZSpan.isAddFundamentalDomain', Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Submodule.fg_iff_addSubgroup_fg, ZLattice.covolume.tendsto_card_le_div', groupHomology.H1AddEquivOfIsTrivial_single, Int.absNorm_under_mem, CommRingCat.coproductCocone_pt, Int.negOnePow_def, instModuleFinite_of_discrete_submodule, Module.Finite.addMonoidHom, PeriodPair.weierstrassP_add_coe, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, ZSpan.span_top, RootPairing.Base.span_int_root_support, NumberField.mixedEmbedding.span_latticeBasis, Subbimodule.coe_toSubbimoduleInt, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, ZSpan.map, ZSpan.exist_unique_vadd_mem_fundamentalDomain, fwdDiff_aux.fwdDiffₗ_apply, Submodule.span_int_eq_addSubgroupClosure, fwdDiff_aux.shiftₗ_apply, PeriodPair.latticeBasis_one, Subbimodule.coe_toSubbimoduleNat, ZLattice.covolume_eq_det_mul_measureReal, PeriodPair.weierstrassP_sub_coe, Differential.mapCoeffs_X, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, NumberField.RingOfIntegers.instFreeInt, ZSpan.isAddFundamentalDomain, Ring.smeval_ascPochhammer_int_ofNat, Profinite.NobelingProof.πs_apply_apply, NumberField.Units.instDiscrete_unitLattice, TensorProduct.CompatibleSMul.int, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, NumberField.absNorm_differentIdeal, ZLattice.exists_forall_abs_repr_le_norm, Profinite.NobelingProof.GoodProducts.linearIndependent, groupHomology.H1AddEquivOfIsTrivial_symm_apply, PeriodPair.hasSum_weierstrassP, PeriodPair.coeff_weierstrassPSeries, PeriodPair.isOpen_compl_lattice_diff, NumberField.fractionalIdeal_rank, Profinite.NobelingProof.GoodProducts.square_commutes, PeriodPair.derivWeierstrassP_coe, Profinite.NobelingProof.Nobeling_aux, groupHomology.H1ToTensorOfIsTrivial_H1π_single, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Profinite.NobelingProof.spanFinBasis.span, Differential.algHom_deriv', AddMonoidHom.coe_toIntLinearMap_ker, ZLattice.covolume.tendsto_card_div_pow', NumberField.inverse_basisMatrix_mulVec_eq_repr, Int.absNorm_under_dvd_absNorm, AddSubgroup.coe_toIntSubmodule, PeriodPair.latticeEquiv_symm_apply, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, AddCommGrpCat.injective_as_module_iff, ZLattice.covolume.tendsto_card_le_div, IsZLattice.span_top, CommRingCat.coproductCoconeIsColimit_desc, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, PeriodPair.analyticOnNhd_derivWeierstrassP, AddMonoidHom.coe_toIntLinearMap_map, AddMonoid.isTorsion_iff_isTorsion_int, Ideal.natAbs_det_equiv, ZSpan.quotientEquiv.symm_apply, NumberField.mem_span_integralBasis, groupHomology.H1AddEquivOfIsTrivial_apply, NumberField.mem_span_basisOfFractionalIdeal, AddMonoidHom.coe_toIntLinearMap_range, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, NonUnitalSubring.unitization_range, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, NumberField.mixedEmbedding.latticeBasis_apply, DistribSMul.toAddMonoidHom_eq_zsmulAddGroupHom, Differential.deriv_aeval_eq, LieModule.coe_lowerCentralSeries_eq_int, Surreal.dyadicMap_apply, Submodule.AddMonoidHom.coe_toIntLinearMap_comap, ZLattice.isAddFundamentalDomain, addMonoidHomLequivInt_symm_apply, instDiscreteTopologySubtypeMemSubmoduleIntComap, Differential.logDeriv_eq_zero, NumberField.mixedEmbedding.latticeBasis_repr_apply, AddMonoid.End.intCast_def, Profinite.NobelingProof.GoodProducts.span_iff_products, Module.Baer.of_divisible, PeriodPair.hasSum_weierstrassPExcept, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Submodule.fg_iff_add_subgroup_fg, FractionalIdeal.abs_det_basis_change, LieModule.IsNilpotent.nilpotent_int, uzpow_intCast, AddSubgroup.toIntSubmodule_toAddSubgroup, Differential.implicitDeriv_X, PeriodPair.differentiableOn_weierstrassPExcept, PeriodPair.derivWeierstrassPExcept_add_coe, NumberField.Units.unitLattice_rank, Profinite.NobelingProof.CC_comp_zero, PeriodPair.differentiableOn_weierstrassP, ZLattice.normBound_spec, Profinite.NobelingProof.eval_eq_πJ, ZSpan.discreteTopology_pi_basisFun, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.Units.logEmbeddingEquiv_apply, ZLattice.covolume.tendsto_card_le_div'', Differential.algEquiv_deriv', NumberField.basisOfFractionalIdeal_apply, PeriodPair.hasSum_sumInvPow, FreeAbelianGroup.instFreeInt, Module.Basis.ofZLatticeComap_repr_apply, PeriodPair.periodic_weierstrassP, Ring.descPochhammer_eq_factorial_smul_choose, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.mkH1OfIsTrivial_apply, tendsto_card_div_pow_atTop_volume', Representation.ofMulDistribMulAction_apply_apply, QuadraticMap.separatingLeft_of_anisotropic, AddMonoidHom.coe_toIntLinearMap, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Profinite.NobelingProof.injective_πs, AddSubgroup.relIndex_eq_natAbs_det, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice, ZSpan.vadd_mem_fundamentalDomain, ZSpan.fract_apply, Profinite.NobelingProof.coe_πs', RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, addMonoidEndRingEquivInt_symm_apply, Int.ideal_span_absNorm_eq_self, AddSubgroup.toIntSubmodule_closure, fwdDiff_aux.coe_fwdDiffₗ_pow, PeriodPair.analyticOnNhd_weierstrassPExcept, Ring.descPochhammer_succ_succ_smeval, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.coe_discr, ZSpan.repr_floor_apply, Module.Finite.iff_addGroup_fg, ModN.instModuleFinite, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, NumberField.mixedEmbedding.disjoint_span_commMap_ker, smul_top_eq_top_of_divisibleBy_int, Int.absNorm_under_eq_sInf, AddMonoidHom.toIntLinearMap_injective, AddMonoid.FG.to_moduleFinite_int, Polynomial.descPochhammer_smeval_eq_ascPochhammer, RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_notMem, mem_nonUnitalSubalgebraOfNonUnitalSubring, ZSpan.fract_eq_fract, ZLattice.sum_piFinset_Icc_rpow_le, Int.cast_mem_ideal_iff, RootPairing.Base.span_int_coroot_support, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, instIsTorsionFreeIntOfIsAddTorsionFree, ZLattice.covolume.tendsto_card_div_pow'', Profinite.NobelingProof.GoodProducts.max_eq_eval, PeriodPair.lattice_eq_span_range_basis, instModuleFree_of_discrete_submodule, PeriodPair.ω₁_mem_lattice, Ideal.natAbs_det_basis_change, PeriodPair.analyticOnNhd_weierstrassP, fwdDiff_aux.coe_fwdDiffₗ, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, Ideal.ringChar_quot, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton, Int.liesOver_span_absNorm, Surreal.dyadicMap_apply_pow, PeriodPair.ω₂_mem_lattice, Profinite.NobelingProof.Products.eval_πs_image, Module.Basis.addSubgroupOfClosure_apply, ZSpan.setFinite_inter, PeriodPair.derivWeierstrassPExcept_def, CommRingCat.coproductCocone_ι, ZLattice.coe_comap, Differential.algEquiv_deriv, NumberField.house.basis_repr_norm_le_const_mul_house, Nat.absNorm_under_prime, PeriodPair.finrank_lattice, PeriodPair.derivWeierstrassP_add_coe, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, Int.submodule_toAddSubgroup_index_ne_zero_iff, BoxIntegral.unitPartition.tag_mem_smul_span, PeriodPair.weierstrassPExcept_add, ZLattice.exists_finsetSum_norm_rpow_le_tsum, ZLattice.abs_repr_le, ZLattice.covolume_eq_det, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply, Submodule.natAbs_det_basis_change, Profinite.NobelingProof.succ_mono, PeriodPair.differentiableOn_derivWeierstrassPExcept
uniqueIntModule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intIsScalarTower 📖	mathematical	—	IsScalarTower SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction toAddCommMonoid	—	Nat.cast_smul_eq_nsmul nsmul_eq_mul SemigroupAction.mul_smul zsmul_eq_mul Int.cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev add_smul neg_smul one_smul negSucc_zsmul

AddCommMonoid

Definitions

Name	Category	Theorems
toNatModule 📖	CompOp	112 math math: Submodule.toAddSubmonoid_toNatSubmodule, DivisibleHull.archimedeanClassMk_mk_eq, iSupIndep.dfinsupp_lsum_injective, Submodule.span_nat_eq_addSubmonoid_closure, Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, MvPowerSeries.weightedOrder_monomial, addMonoidHomLequivNat_symm_apply, QuadraticMap.canLift, MvPolynomial.weightedDegree_eq_zero_iff, ComplexShape.eulerCharSignsDownNat_χ, OreLocalization.nsmul_eq_nsmul, Finsupp.le_weight_of_ne_zero', uzpow_natCast, Fintype.linearIndependent_iff', DivisibleHull.mk_add_mk_left, MvPolynomial.le_weightedTotalDegree, uzpow_coe_nat, Submodule.biSup_eq_range_dfinsupp_lsum, AddMonoidHom.toNatLinearMap_injective, AddEquiv.toNatLinearEquiv_toAddEquiv, MvPowerSeries.weightedOrder_monomial_of_ne_zero, ComplexShape.ε_down_ℕ, Submodule.span_nat_eq, AddSubmonoid.toNatSubmodule_toAddSubmonoid, AddSubmonoid.toNatSubmodule_closure, NonUnitalSubsemiring.unitization_apply, Polynomial.smeval_neg_nat, DFinsupp.sum_mapRange_index.linearMap, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, Submodule.mem_iSup_iff_exists_dfinsupp, Submodule.iSup_eq_range_dfinsupp_lsum, DivisibleHull.instIsStrictOrderedModuleNNRat, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, Finsupp.finite_of_nat_weight_le, Finsupp.le_weight, Module.isTorsionFree_nat_iff_isAddTorsionFree, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Fintype.linearIndependent_iff'ₛ, AddEquiv.toNatLinearEquiv_trans, AddMonoidHom.coe_toNatLinearMap, MvPowerSeries.le_weightedOrder_subst, isProperLinearSet_iff, Polynomial.smeval_at_natCast, AddMonoid.FG.to_moduleFinite_nat, DivisibleHull.coeAddMonoidHom_apply, DivisibleHull.instIsOrderedCancelAddMonoid, MvPowerSeries.coeff_weightedHomogeneousComponent, Ring.ascPochhammer_succ_succ, AddSubmonoid.toNatSubmodule_symm, BinomialRing.factorial_nsmul_multichoose, Subbimodule.coe_toSubbimoduleInt, Module.End.natCast_def, AddMonoid.End.natCast_def, DivisibleHull.qsmul_def, Subbimodule.coe_toSubbimoduleNat, Ring.smeval_ascPochhammer_int_ofNat, QuadraticMap.canLift', DivisibleHull.qsmul_of_nonneg, Ring.smeval_ascPochhammer_nat_cast, DivisibleHull.coeOrderAddMonoidHom_apply, Submodule.fg_iff_addSubmonoid_fg, AddCommGroup.DirectLimit.directedSystem, DivisibleHull.nsmul_mk, Polynomial.ascPochhammer_smeval_cast, MvPowerSeries.weightedOrder_eq_nat, Nat.instIsNoetherian, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, Submodule.span_nat_eq_addSubmonoidClosure, MvPowerSeries.weightedOrder_le, AddEquiv.toNatLinearEquiv_refl, Matrix.toLinearMap₂'_single, ComplexShape.eulerCharSignsUpNat_χ, DivisibleHull.mk_add_mk, MvPolynomial.weightedDecomposition.decompose'_eq, Finsupp.le_weight_of_ne_zero, Ring.smeval_ascPochhammer_neg_add, Module.Basis.toMatrix_eq_toMatrix_constr, DivisibleHull.archimedeanClassOrderIso_apply, AddEquiv.coe_symm_toNatLinearEquiv, addMonoidHomLequivNat_apply, AddMonoid.isTorsion_iff_isTorsion_nat, DivisibleHull.zsmul_mk, iSupIndep_iff_dfinsupp_lsum_injective, Ring.smeval_ascPochhammer_succ_neg, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, DivisibleHull.neg_mk, NonUnitalSubsemiring.unitization_range, AddSubmonoid.coe_toNatSubmodule, DivisibleHull.qsmul_of_nonpos, Polynomial.ascPochhammer_smeval_eq_eval, Finsupp.weight_sub_single_add, DivisibleHull.archimedeanClassOrderIso_symm_apply, AddEquiv.coe_toNatLinearEquiv, DivisibleHull.instIsStrictOrderedModuleRat, Ring.smeval_ascPochhammer_neg_of_lt, DivisibleHull.coe_add, Module.Finite.iff_addMonoid_fg, mem_nonUnitalSubalgebraOfNonUnitalSubsemiring, DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom, DivisibleHull.mk_zero, DivisibleHull.zero_qsmul, LinearEquiv.toAddEquiv_toNatLinearEquiv, AddEquiv.toNatLinearEquiv_symm, MvPolynomial.coeff_weightedHomogeneousComponent, Submodule.mem_biSup_iff_exists_dfinsupp, Polynomial.descPochhammer_smeval_eq_ascPochhammer, Ring.smeval_ascPochhammer_self_neg, Finsupp.weight_eq_zero_iff_eq_zero, MvPolynomial.weightedHomogeneousComponent_apply, DivisibleHull.nnqsmul_mk, lsum_comp_mapRange_toSpanSingleton, IsAddTorsionFree.to_isTorsionFree_nat
uniqueNatModule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_isScalarTower 📖	mathematical	—	IsScalarTower AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	zero_smul add_smul one_smul
subsingletonIntModule 📖	mathematical	—	Module Int.instSemiring	—	Unique.instSubsingleton
subsingletonNatModule 📖	mathematical	—	Module Nat.instSemiring	—	Unique.instSubsingleton

CharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_module 📖	mathematical	—	CharZero AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Nat.cast_injective nsmul_one Nat.cast_smul_eq_nsmul

DistribSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddMonoidHom_eq_nsmulAddMonoidHom 📖	mathematical	—	toAddMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul Nat.instMonoid Module.toDistribMulAction Nat.instSemiring AddCommMonoid.toNatModule nsmulAddMonoidHom	—	—
toAddMonoidHom_eq_zsmulAddGroupHom 📖	mathematical	—	toAddMonoidHom AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul Int.instMonoid Module.toDistribMulAction Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid	—	—

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_smul_eq_zsmul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne SubNegMonoid.toZSMul	—	cast_natCast Nat.cast_smul_eq_nsmul cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev add_smul neg_smul one_smul negSucc_zsmul
smul_one_eq_cast 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast	—	zsmul_eq_mul mul_one

Module

Definitions

Name	Category	Theorems
addCommMonoidToAddCommGroup 📖	CompOp	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_smul_eq_nsmul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoid.toNatSMul	—	cast_zero zero_smul cast_succ add_smul one_smul
smul_one_eq_cast 📖	mathematical	—	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidWithOne.toOne AddMonoidWithOne.toNatCast	—	nsmul_eq_mul mul_one

(root)

Definitions

Name	Category	Theorems
instMulActionIntOfSubtractionMonoid 📖	CompOp	—
instMulActionNatOfAddMonoid 📖	CompOp	—
instSMulWithZeroInt 📖	CompOp	1 math math: Int.orderedSMul
instSMulWithZeroNat 📖	CompOp	1 math math: Nat.orderedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
int_smul_eq_zsmul 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Int.instSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Int.cast_smul_eq_zsmul
map_intCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	Int.cast_smul_eq_zsmul map_zsmul
map_natCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Nat.cast_smul_eq_nsmul map_nsmul
nat_smul_eq_nsmul 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AddMonoid.toNatSMul	—	Nat.cast_smul_eq_nsmul
ofNat_smul_eq_nsmul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoid.toNatSMul	—	Nat.cast_smul_eq_nsmul

---

← Back to Index