RingHoms

📁 Source: Mathlib/NumberTheory/Padics/RingHoms.lean

Statistics

Metric	Count
Definitions appr, limNthHom, modPart, nthHom, nthHomSeq, residueField, toZMod, toZModHom, toZModPow, zmodRepr	10
Theorems appr_lt, appr_mono, appr_spec, cast_toZModPow, denseRange_intCast, denseRange_natCast, dvd_appr_sub_appr, existsUnique_mem_range, exists_mem_range, exists_mem_range_of_norm_rat_le_one, ext_of_toZModPow, isCauSeq_nthHom, isCauSeq_padicNorm_of_pow_dvd_sub, ker_toZMod, ker_toZModPow, lift_self, lift_spec, lift_sub_val_mem_span, lift_unique, limNthHom_add, limNthHom_mul, limNthHom_one, limNthHom_spec, limNthHom_zero, modPart_lt_p, modPart_nonneg, norm_natCast_zmodRepr_eq, norm_natCast_zmodRepr_eq_iff, norm_natCast_zmodRepr_eq_one_iff, norm_natCast_zmodRepr_eq_one_iff_ne, norm_sub_modPart, norm_sub_modPart_aux, norm_sub_zmodRepr_lt_one, nthHomSeq_add, nthHomSeq_mul, nthHomSeq_one, nthHom_zero, pow_dvd_nthHom_sub, sub_zmodRepr_mem, toZModPow_eq_iff_ext, toZModPow_ofIntSeq_of_pow_dvd_sub, toZMod_eq_residueField_comp_residue, toZMod_spec, val_toZMod_eq_zmodRepr, zmodRepr_eq_zero_iff_dvd, zmodRepr_eq_zero_of_dvd, zmodRepr_lt_p, zmodRepr_mul, zmodRepr_natCast, zmodRepr_natCast_ofNat, zmodRepr_natCast_of_lt, zmodRepr_natCast_zmodRepr, zmodRepr_spec, zmodRepr_unique, zmodRepr_units_ne_zero, zmodRepr_zero, zmod_cast_comp_toZModPow, zmod_congr_of_sub_mem_max_ideal, zmod_congr_of_sub_mem_span, zmod_congr_of_sub_mem_span_aux	60
Total	70

PadicInt

Definitions

Name	Category	Theorems
appr 📖	CompOp	4 math math: appr_spec, appr_mono, appr_lt, dvd_appr_sub_appr
limNthHom 📖	CompOp	5 math math: limNthHom_spec, limNthHom_add, limNthHom_one, limNthHom_mul, limNthHom_zero
modPart 📖	CompOp	3 math math: modPart_nonneg, modPart_lt_p, norm_sub_modPart
nthHom 📖	CompOp	4 math math: isCauSeq_nthHom, nthHom_zero, pow_dvd_nthHom_sub, limNthHom_spec
nthHomSeq 📖	CompOp	3 math math: nthHomSeq_mul, nthHomSeq_add, nthHomSeq_one
residueField 📖	CompOp	1 math math: toZMod_eq_residueField_comp_residue
toZMod 📖	CompOp	4 math math: toZMod_eq_residueField_comp_residue, ker_toZMod, val_toZMod_eq_zmodRepr, toZMod_spec
toZModHom 📖	CompOp	—
toZModPow 📖	CompOp	13 math math: cyclotomicCharacter.toZModPow, ext_of_toZModPow, toZModPow_ofIntSeq_of_pow_dvd_sub, zmod_cast_comp_toZModPow, toZModPow_eq_iff_ext, ker_toZModPow, cyclotomicCharacter.toZModPow_toFun, lift_spec, cyclotomicCharacter.spec, cast_toZModPow, WittVector.zmodEquivTrunc_compat, cyclotomicCharacter.toFun_spec, lift_self
zmodRepr 📖	CompOp	18 math math: sub_zmodRepr_mem, zmodRepr_mul, norm_natCast_zmodRepr_eq_one_iff_ne, zmodRepr_natCast_ofNat, zmodRepr_unique, zmodRepr_spec, norm_natCast_zmodRepr_eq_one_iff, zmodRepr_natCast, norm_natCast_zmodRepr_eq, zmodRepr_zero, zmodRepr_lt_p, zmodRepr_natCast_zmodRepr, norm_sub_zmodRepr_lt_one, zmodRepr_eq_zero_of_dvd, norm_natCast_zmodRepr_eq_iff, zmodRepr_natCast_of_lt, val_toZMod_eq_zmodRepr, zmodRepr_eq_zero_iff_dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
appr_lt 📖	mathematical	—	appr Monoid.toNatPow Nat.instMonoid	—	pow_zero Nat.instZeroLEOneClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_natCast ZMod.natCast_self Nat.Prime.one_lt Fact.out lt_trans add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add ZMod.val_lt NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' mul_tsub Nat.instOrderedSub LE.total IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le mul_one pow_succ add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE le_of_lt
appr_mono 📖	mathematical	—	Monotone Nat.instPreorder appr	—	monotone_nat_of_le_succ le_refl
appr_spec 📖	mathematical	—	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing appr	—	pow_zero dvd_zero Nat.cast_add Nat.cast_mul Nat.cast_pow sub_add_eq_sub_sub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_natCast ZMod.natCast_self ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' MulZeroClass.mul_zero valuation_p_pow_mul add_sub_cancel_left pow_succ mul_sub mul_dvd_mul_left eq_or_ne Nat.cast_zero mul_one CanLift.prf instCanLiftUnitsValIsUnit norm_eq_zpow_neg_valuation CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero neg_zero zpow_zero IsDiscreteValuationRing.unit_mul_pow_congr_unit instIsDomain instIsDiscreteValuationRing irreducible_p unitCoeff_spec mul_comm Ideal.mem_span_singleton instIsLocalRing maximalIdeal_eq_span_p toZMod_spec zero_pow ZMod.cast_zero sub_zero Dvd.dvd.mul_left dvd_pow_self
cast_toZModPow 📖	mathematical	—	ZMod.cast ZMod Monoid.toNatPow Nat.instMonoid Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing DFunLike.coe RingHom PadicInt Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike toZModPow	—	pow_dvd_pow ZMod.charP zmod_cast_comp_toZModPow
denseRange_intCast 📖	mathematical	—	DenseRange PadicInt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	DenseRange.induction_on denseRange_natCast isClosed_closure subset_closure Set.mem_range_self
denseRange_natCast 📖	mathematical	—	DenseRange PadicInt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	Metric.mem_closure_range_iff exists_pow_neg_lt dist_eq_norm lt_of_le_of_lt norm_le_pow_iff_mem_span_pow appr_spec
dvd_appr_sub_appr 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid appr	—	add_zero tsub_eq_zero_of_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_assoc add_comm add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le appr_mono dvd_add Distrib.leftDistribClass dvd_mul_of_dvd_left pow_dvd_pow
existsUnique_mem_range 📖	mathematical	—	ExistsUnique PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	instIsLocalRing exists_mem_range zmod_congr_of_sub_mem_max_ideal Nat.ModEq.eq_1 ZMod.natCast_eq_natCast_iff
exists_mem_range 📖	mathematical	—	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	instIsLocalRing maximalIdeal_eq_span_p Padic.rat_dense zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Padic.nonarchimedean max_le le_of_lt norm_sub_rev exists_mem_range_of_norm_rat_le_one CanLift.prf instCanLiftIntNatCastLeOfNat Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero lt_of_le_of_lt max_lt Int.cast_natCast
exists_mem_range_of_norm_rat_le_one 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField Real.instOne	Real.instLT PadicInt instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	modPart_nonneg modPart_lt_p norm_sub_modPart
ext_of_toZModPow 📖	mathematical	—	DFunLike.coe RingHom PadicInt ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing ZMod.commRing RingHom.instFunLike toZModPow	—	zmod_cast_comp_toZModPow lift_self Rat.instIsStrictOrderedRing isCauSeq_nthHom ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' limNthHom_one ofIntSeq.congr_simp limNthHom_mul limNthHom_zero limNthHom_add
isCauSeq_nthHom 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm nthHom	—	pow_dvd_pow ZMod.charP exists_pow_neg_lt_rat lt_of_le_of_lt padicNorm.dvd_iff_norm_le pow_dvd_nthHom_sub
isCauSeq_padicNorm_of_pow_dvd_sub 📖	mathematical	Monoid.toNatPow Int.instMonoid	IsCauSeq Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm	—	exists_pow_neg_lt_rat LE.le.trans_lt padicNorm.dvd_iff_norm_le ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.cast_pow add_zero sub_self pow_add sub_add_sub_cancel Dvd.dvd.add Distrib.leftDistribClass Dvd.dvd.trans
ker_toZMod 📖	mathematical	—	RingHom.ker PadicInt ZMod RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField RingHom.instFunLike RingHom.instRingHomClass toZMod IsLocalRing.maximalIdeal instIsLocalRing	—	Ideal.ext RingHom.instRingHomClass instIsLocalRing RingHom.mem_ker ZMod.cast_zero sub_zero toZMod_spec Nat.cast_zero zmod_congr_of_sub_mem_max_ideal sub_zmodRepr_mem
ker_toZModPow 📖	mathematical	—	RingHom.ker PadicInt ZMod Monoid.toNatPow Nat.instMonoid RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing ZMod.commRing RingHom.instFunLike RingHom.instRingHomClass toZModPow Ideal.span Set Set.instSingletonSet MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	Ideal.ext RingHom.instRingHomClass RingHom.mem_ker ZMod.natCast_eq_zero_iff appr_lt Nat.cast_zero sub_zero appr_spec zmod_congr_of_sub_mem_span
lift_self 📖	mathematical	—	DFunLike.coe RingHom PadicInt Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike lift toZModPow zmod_cast_comp_toZModPow	—	zmod_cast_comp_toZModPow lift_unique RingHom.comp_id
lift_spec 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	PadicInt instCommRing toZModPow lift	—	pow_dvd_pow ZMod.charP RingHom.ext RingHom.comp_apply ZMod.natCast_zmod_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' map_natCast RingHom.instRingHomClass sub_eq_zero map_sub RingHomClass.toAddMonoidHomClass RingHom.mem_ker ker_toZModPow lift_sub_val_mem_span
lift_sub_val_mem_span 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	PadicInt Ideal instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe RingHom RingHom.instFunLike lift ZMod.val	—	pow_dvd_pow ZMod.charP limNthHom_spec zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.pos Fact.out le_of_lt le_max_right sub_eq_sub_add_sub Ideal.add_mem Ideal.mem_span_singleton eq_intCast RingHom.instRingHomClass Int.cast_pow Int.cast_natCast ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.intCast_cast Int.cast_sub map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass pow_dvd_nthHom_sub le_max_left norm_le_pow_iff_mem_span_pow
lift_unique 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP PadicInt instCommRing toZModPow	lift	—	pow_dvd_pow ZMod.charP RingHom.ext eq_of_forall_dist_le exists_pow_neg_lt le_trans dist_eq_norm norm_le_pow_iff_mem_span_pow RingHom.instRingHomClass ker_toZModPow RingHom.mem_ker map_sub RingHomClass.toAddMonoidHomClass RingHom.comp_apply lift_spec sub_self le_of_lt
limNthHom_add 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	limNthHom Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring PadicInt NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat isCauSeq_nthHom nthHomSeq_add
limNthHom_mul 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	limNthHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring PadicInt NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat isCauSeq_nthHom nthHomSeq_mul
limNthHom_one 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	limNthHom AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne PadicInt AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat isCauSeq_nthHom nthHomSeq_one
limNthHom_spec 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP Real Real.instLT Real.instZero	Norm.norm PadicInt instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing limNthHom AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing nthHom	—	pow_dvd_pow ZMod.charP exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean Rat.instIsStrictOrderedRing padicNormE.defn Nat.cast_zero lt_trans
limNthHom_zero 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	limNthHom MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring PadicInt NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing isCauSeq_nthHom nthHom_zero ofIntSeq.congr_simp
modPart_lt_p 📖	mathematical	—	modPart	—	Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.emod_lt_abs Nat.cast_zero Int.instCharZero Nat.Prime.ne_zero Fact.out
modPart_nonneg 📖	mathematical	—	modPart	—	Nat.cast_zero Int.instCharZero Nat.Prime.ne_zero Fact.out
norm_natCast_zmodRepr_eq 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing zmodRepr Real Real.instOne	—	—
norm_natCast_zmodRepr_eq_iff 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing zmodRepr Real Real.instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	norm_natCast_zmodRepr_eq norm_zero zmodRepr_zero CharP.cast_eq_zero CharP.ofCharZero instCharZero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
norm_natCast_zmodRepr_eq_one_iff 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing zmodRepr Real Real.instOne	—	eq_or_ne norm_sub_zmodRepr_lt_one Padic.norm_eq_of_norm_sub_lt_right Padic.norm_eq_of_norm_sub_lt_left
norm_natCast_zmodRepr_eq_one_iff_ne 📖	mathematical	—	Norm.norm PadicInt instNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing zmodRepr Real Real.instOne	—	norm_natCast_zmodRepr_eq_one_iff zmodRepr_eq_zero_iff_dvd norm_lt_one_iff_dvd
norm_sub_modPart 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField Real.instOne	Real.instLT PadicInt instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing modPart	—	norm_lt_one_iff_dvd IsUnit.dvd_mul_right isUnit_den norm_sub_modPart_aux sub_mul eq_intCast RingHom.instRingHomClass Int.cast_sub Int.cast_mul Int.cast_natCast Subtype.coe_injective Rat.cast_natCast Padic.instCharZero Rat.mul_den_eq_num Rat.cast_intCast map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
norm_sub_modPart_aux 📖	mathematical	Real Real.instLE Norm.norm Padic Padic.instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField Real.instOne	Nat.gcdA	—	ZMod.intCast_zmod_eq_zero_iff_dvd Int.cast_sub Int.cast_mul Int.cast_natCast Nat.gcd_eq_gcd_ab ZMod.intCast_mod mul_right_comm mul_assoc CharP.cast_eq_zero ZMod.charP EuclideanDomain.mod_zero Int.cast_add MulZeroClass.zero_mul add_zero Nat.coprime_or_dvd_of_prime Fact.out norm_int_lt_one_iff_dvd not_lt ge_of_eq isUnit_iff isUnit_den Nat.cast_one mul_one sub_self
norm_sub_zmodRepr_lt_one 📖	mathematical	—	Real Real.instLT Norm.norm PadicInt instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing zmodRepr Real.instOne	—	mem_nonunits instIsLocalRing IsLocalRing.mem_maximalIdeal sub_zmodRepr_mem
nthHomSeq_add 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat nthHomSeq Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CauSeq.instAdd	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat exists_pow_neg_lt_rat lt_of_le_of_lt Int.cast_add Int.cast_sub padicNorm.dvd_iff_norm_le ZMod.intCast_zmod_eq_zero_iff_dvd map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.intCast_cast ZMod.cast_add sub_self
nthHomSeq_mul 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat nthHomSeq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CauSeq.instMul	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat exists_pow_neg_lt_rat lt_of_le_of_lt Int.cast_mul Int.cast_sub padicNorm.dvd_iff_norm_le ZMod.intCast_zmod_eq_zero_iff_dvd map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.intCast_cast ZMod.cast_mul sub_self
nthHomSeq_one 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	PadicSeq CauSeq.equiv Rat.instField Rat.linearOrder Rat.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField padicNorm padicNorm.instIsAbsoluteValueRat nthHomSeq AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CauSeq.instOne	—	pow_dvd_pow ZMod.charP Rat.instIsStrictOrderedRing padicNorm.instIsAbsoluteValueRat ZMod.cast_eq_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.val_one Nat.Prime.one_lt Fact.out Nat.cast_one isCauSeq_nthHom map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass ZMod.natCast_val ZMod.intCast_cast sub_self padicNorm.zero
nthHom_zero 📖	mathematical	—	nthHom MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.instZero NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass ZMod.val_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero
pow_dvd_nthHom_sub 📖	mathematical	RingHom.comp ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP	Int.instMonoid nthHom	—	pow_dvd_pow ZMod.charP ZMod.intCast_zmod_eq_zero_iff_dvd Int.cast_sub RingHom.comp_apply ZMod.natCast_val NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ZMod.intCast_cast ZMod.cast_id sub_self
sub_zmodRepr_mem 📖	mathematical	—	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing zmodRepr	—	instIsLocalRing zmodRepr_spec
toZModPow_eq_iff_ext 📖	mathematical	—	RingHom.comp PadicInt ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing ZMod.commRing toZModPow	—	RingHom.ext ext_of_toZModPow
toZModPow_ofIntSeq_of_pow_dvd_sub 📖	mathematical	Monoid.toNatPow Int.instMonoid	DFunLike.coe RingHom PadicInt ZMod Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing ZMod.commRing RingHom.instFunLike toZModPow ofIntSeq isCauSeq_padicNorm_of_pow_dvd_sub AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	isCauSeq_padicNorm_of_pow_dvd_sub Rat.instIsStrictOrderedRing Ideal.mem_span_singleton appr_spec padicNormE.defn zpow_neg zpow_natCast PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' LE.le.trans_lt norm_mul NormedDivisionRing.toNormMulClass Padic.norm_p_pow padic_norm_e_of_padicInt mul_one mul_le_mul_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_rfl Real.instIsStrictOrderedRing Real.instZeroLEOneClass zero_le_one lt_asymm sup_eq_right LT.lt.le Padic.add_eq_max_of_ne LT.lt.ne Int.cast_natCast Rat.cast_intCast Rat.cast_zpow IsStrictOrderedRing.toCharZero Rat.cast_natCast Rat.cast_lt sub_eq_iff_eq_add ZMod.intCast_eq_intCast_iff_dvd_sub Nat.cast_pow Padic.norm_int_le_pow_iff_dvd zero_add add_right_comm Dvd.dvd.trans pow_add mul_comm
toZMod_eq_residueField_comp_residue 📖	mathematical	—	toZMod RingHom.comp PadicInt IsLocalRing.ResidueField instCommRing instIsLocalRing ZMod Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field ZMod.instField RingEquiv.toRingHom residueField IsLocalRing.residue	—	—
toZMod_spec 📖	mathematical	—	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing ZMod.cast Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing DFunLike.coe RingHom ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField RingHom.instFunLike toZMod	—	instIsLocalRing Nat.Prime.pos Fact.out instCharZero zero_add zmodRepr_lt_p sub_zmodRepr_mem
val_toZMod_eq_zmodRepr 📖	mathematical	—	ZMod.val DFunLike.coe RingHom PadicInt ZMod Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField RingHom.instFunLike toZMod zmodRepr	—	zmodRepr_unique ZMod.val_lt NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' instIsLocalRing ZMod.natCast_val toZMod_spec
zmodRepr_eq_zero_iff_dvd 📖	mathematical	—	zmodRepr PadicInt semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	norm_lt_one_iff_dvd sub_zero Nat.cast_zero norm_sub_zmodRepr_lt_one zmodRepr_eq_zero_of_dvd
zmodRepr_eq_zero_of_dvd 📖	mathematical	PadicInt semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	zmodRepr	—	zmodRepr_unique Nat.Prime.pos Fact.out instIsLocalRing maximalIdeal_eq_span_p CharP.cast_eq_zero CharP.ofCharZero instCharZero sub_zero
zmodRepr_lt_p 📖	mathematical	—	zmodRepr	—	instIsLocalRing zmodRepr_spec
zmodRepr_mul 📖	mathematical	—	zmodRepr PadicInt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass ZMod.val_mul
zmodRepr_natCast 📖	mathematical	—	zmodRepr PadicInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	zmodRepr_unique Nat.Prime.pos Fact.out instIsLocalRing maximalIdeal_eq_span_p Nat.cast_add Nat.cast_mul add_sub_cancel_left
zmodRepr_natCast_ofNat 📖	mathematical	—	zmodRepr	—	CharP.cast_eq_zero CharP.ofCharZero instCharZero Nat.cast_one zmodRepr_natCast_of_lt
zmodRepr_natCast_of_lt 📖	mathematical	—	zmodRepr PadicInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	zmodRepr_natCast
zmodRepr_natCast_zmodRepr 📖	mathematical	—	zmodRepr PadicInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing	—	zmodRepr_unique zmodRepr_lt_p instIsLocalRing sub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
zmodRepr_spec 📖	mathematical	—	zmodRepr PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	instIsLocalRing ExistsUnique.exists existsUnique_mem_range
zmodRepr_unique 📖	mathematical	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	zmodRepr	—	instIsLocalRing existsUnique_mem_range zmodRepr_spec
zmodRepr_units_ne_zero 📖	—	—	—	—	zmodRepr_eq_zero_iff_dvd Irreducible.not_dvd_isUnit irreducible_p Units.isUnit
zmodRepr_zero 📖	mathematical	—	zmodRepr PadicInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing	—	zmodRepr_eq_zero_of_dvd dvd_zero
zmod_cast_comp_toZModPow 📖	mathematical	—	RingHom.comp PadicInt ZMod Monoid.toNatPow Nat.instMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing ZMod.commRing Ring.toSemiring CommRing.toRing ZMod.castHom pow_dvd_pow ZMod.charP toZModPow	—	ZMod.ringHom_eq_of_ker_eq pow_dvd_pow ZMod.charP Ideal.ext RingHom.instRingHomClass RingHom.mem_ker ZMod.cast_natCast zmod_congr_of_sub_mem_span sub_self Ideal.zero_mem Ideal.mem_span_singleton dvd_appr_sub_appr Nat.cast_sub appr_mono Nat.cast_mul Nat.cast_pow
zmod_congr_of_sub_mem_max_ideal 📖	mathematical	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal instIsLocalRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing instNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	ZMod DivisionRing.toRing Field.toDivisionRing ZMod.instField	—	instIsLocalRing zmod_congr_of_sub_mem_span_aux Int.cast_natCast pow_one dvd_refl ZMod.charP map_intCast RingHom.instRingHomClass maximalIdeal_eq_span_p
zmod_congr_of_sub_mem_span 📖	mathematical	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	ZMod Nat.instMonoid CommRing.toRing ZMod.commRing	—	Int.cast_natCast zmod_congr_of_sub_mem_span_aux
zmod_congr_of_sub_mem_span_aux 📖	mathematical	PadicInt Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing instNormedCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddGroupWithOne.toIntCast	ZMod Nat.instMonoid CommRing.toRing ZMod.commRing	—	sub_eq_zero Int.cast_sub ZMod.intCast_zmod_eq_zero_iff_dvd dvd_add Distrib.leftDistribClass neg_sub dvd_neg Ideal.mem_span_singleton pow_p_dvd_int_iff sub_eq_add_neg neg_add_cancel_left add_assoc

---

← Back to Index