PadicNorm

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

Statistics

Metric	Count
Definitions padicNorm	1
Theorems add_eq_max_of_ne, div, dvd_iff_norm_le, eq_zpow_of_nonzero, instIsAbsoluteValueRat, int_eq_one_iff, int_lt_one_iff, mul, nat_eq_one_iff, nat_lt_one_iff, neg, nonarchimedean, nonneg, nonzero, not_int_of_not_padic_int, of_int, of_nat, one, padicNorm_of_prime_of_ne, padicNorm_p, padicNorm_p_lt_one, padicNorm_p_lt_one_of_prime, padicNorm_p_of_prime, sub, sum_le, sum_le', sum_lt, sum_lt', triangle_ineq, values_discrete, zero, zero_of_padicNorm_eq_zero	32
Total	33

(root)

Definitions

Name	Category	Theorems
padicNorm 📖	CompOp	60 math math: padicNorm.instIsAbsoluteValueRat, padicNorm.padicNorm_p_lt_one_of_prime, Padic.eq_padicNorm, PadicInt.isCauSeq_nthHom, padicNorm.int_eq_one_iff, PadicSeq.ne_zero_iff_nequiv_zero, padicNorm.padicNorm_p_of_prime, padicNorm.nonarchimedean, Padic.exi_rat_seq_conv_cauchy, padicNorm.mul, padicNormE.eq_padic_norm', Padic.zero_def, padicNorm.int_lt_one_iff, padicNorm.padicNorm_p, PadicSeq.lift_index_left_left, padicNormE.defn, PadicSeq.lift_index_right, padicNorm.nat_lt_one_iff, PadicSeq.norm_neg, padicNorm.sub, padicNorm.eq_zpow_of_nonzero, PadicSeq.norm_nonarchimedean, PadicSeq.not_equiv_zero_const_of_nonzero, padicNorm.triangle_ineq, padicNorm.div, Rat.AbsoluteValue.padic_eq_padicNorm, padicNorm.of_nat, PadicSeq.equiv_zero_of_val_eq_of_equiv_zero, PadicInt.nthHomSeq_mul, padicNorm.one, Padic.mk_eq, padicNorm.values_discrete, padicNorm.dvd_iff_norm_le, padicNorm.nonneg, padicNorm.add_eq_max_of_ne, padicNorm.nat_eq_one_iff, PadicSeq.not_limZero_const_of_nonzero, padicNorm.sum_lt, PadicSeq.stationaryPoint_spec, padicNorm.padicNorm_p_lt_one, padicNorm.neg, PadicSeq.lift_index_left, padicNorm.of_int, PadicSeq.norm_eq_norm_app_of_nonzero, PadicSeq.add_eq_max_of_ne, PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub, PadicInt.nthHomSeq_add, PadicInt.nthHomSeq_one, PadicSeq.norm_const, PadicSeq.norm_one, padicNorm.zero, PadicSeq.norm_zero_iff, padicNorm.padicNorm_of_prime_of_ne, PadicSeq.stationary, padicNorm.sum_le, PadicSeq.norm_mul, Padic.const_equiv, padicNorm.sum_le', PadicSeq.eq_zero_iff_equiv_zero, padicNorm.sum_lt'

padicNorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_max_of_ne 📖	mathematical	—	padicNorm Rat.instSup	—	Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr 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_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 nonarchimedean neg le_of_not_gt not_lt_of_ge max_eq_right_of_lt max_eq_left le_antisymm max_eq_left_of_lt add_comm max_comm Ne.lt_or_gt
div 📖	mathematical	—	padicNorm	—	div_zero zero eq_div_of_mul_eq nonzero mul div_mul_cancel₀
dvd_iff_norm_le 📖	mathematical	—	Monoid.toPow Nat.instMonoid padicNorm	—	Nat.cast_pow Nat.cast_zero Int.cast_zero Rat.instCharZero zpow_neg zpow_natCast PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Rat.instZeroLEOneClass Rat.instPosMulMono IsStrictOrderedRing.toIsOrderedRing zpow_le_zpow_iff_right₀ Nat.cast_one Rat.instAddLeftMono Nat.Prime.one_lt Fact.out neg_le_neg_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add padicValRat.of_int padicValInt.of_ne_one_ne_zero Nat.Prime.ne_one Int.instZeroLEOneClass Int.instCharZero FiniteMultiplicity.pow_dvd_iff_le_multiplicity Int.finiteMultiplicity_iff
eq_zpow_of_nonzero 📖	mathematical	—	padicNorm padicValRat	—	zpow_neg
instIsAbsoluteValueRat 📖	mathematical	—	IsAbsoluteValue Rat.semiring Rat.instPartialOrder padicNorm	—	nonneg zero_of_padicNorm_eq_zero zero triangle_ineq mul
int_eq_one_iff 📖	mathematical	—	padicNorm	—	pow_one Nat.cast_one zpow_neg zpow_one inv_lt_one₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_zero Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero Nat.Prime.pos Fact.out Nat.Prime.one_lt inv_lt_zero Rat.instPosMulMono Nat.cast_lt zpow_neg_one zpow_lt_zpow_iff_right₀ padicValRat.of_int IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing zpow_zero zpow_right_inj₀ lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Rat.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Int.instIsOrderedAddMonoid
int_lt_one_iff 📖	mathematical	—	padicNorm	—	not_iff_not int_eq_one_iff eq_iff_le_not_lt
mul 📖	mathematical	—	padicNorm	—	MulZeroClass.zero_mul zero MulZeroClass.mul_zero Rat.instCharZero Nat.Prime.ne_zero Fact.out IsDomain.to_noZeroDivisors Rat.isDomain padicValRat.mul neg_add_rev zpow_add₀ zpow_neg mul_comm
nat_eq_one_iff 📖	mathematical	—	padicNorm	—	int_eq_one_iff Int.cast_natCast
nat_lt_one_iff 📖	mathematical	—	padicNorm	—	int_lt_one_iff Int.cast_natCast
neg 📖	mathematical	—	padicNorm	—	neg_zero zero padicValRat.neg zpow_neg
nonarchimedean 📖	mathematical	—	padicNorm Rat.instSup	—	add_comm max_comm le_of_not_ge
nonneg 📖	mathematical	—	padicNorm	—	instReflLe zpow_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Rat.instZeroLEOneClass Nat.cast_zero Rat.instAddLeftMono Rat.instCharZero
nonzero 📖	—	—	—	—	eq_zpow_of_nonzero zpow_ne_zero Nat.cast_zero Rat.instCharZero ne_of_gt Nat.Prime.pos Fact.out
not_int_of_not_padic_int 📖	—	padicNorm	—	—	Mathlib.Tactic.Contrapose.contrapose₃ Rat.eq_num_of_isInt of_int
of_int 📖	mathematical	—	padicNorm	—	eq_or_ne Int.cast_zero zero Rat.instZeroLEOneClass eq_1 Nat.cast_zero Rat.instCharZero zpow_le_one_of_nonpos₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_one Rat.instAddLeftMono Nat.Prime.one_le Fact.out padicValRat.of_int Int.instAddLeftMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing
of_nat 📖	mathematical	—	padicNorm	—	of_int
one 📖	mathematical	—	padicNorm	—	NeZero.charZero_one Rat.instCharZero padicValRat.one neg_zero zpow_zero
padicNorm_of_prime_of_ne 📖	mathematical	—	padicNorm	—	Nat.cast_zero Int.instCharZero padicValNat_primes eq_1 Rat.instCharZero Nat.Prime.ne_zero Fact.out neg_zero zpow_zero
padicNorm_p 📖	mathematical	—	padicNorm	—	Rat.instCharZero LT.lt.ne' pos_of_gt Nat.instCanonicallyOrderedAdd padicValRat.of_nat padicValNat.self Nat.cast_one zpow_neg zpow_one
padicNorm_p_lt_one 📖	mathematical	—	padicNorm	—	padicNorm_p inv_lt_one_iff₀ IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Rat.instZeroLEOneClass Nat.cast_zero Nat.cast_one Rat.instAddLeftMono Rat.instCharZero
padicNorm_p_lt_one_of_prime 📖	mathematical	—	padicNorm	—	padicNorm_p_lt_one Nat.Prime.one_lt Fact.out
padicNorm_p_of_prime 📖	mathematical	—	padicNorm	—	padicNorm_p Nat.Prime.one_lt Fact.out
sub 📖	mathematical	—	padicNorm Rat.instSup	—	sub_eq_add_neg neg nonarchimedean
sum_le 📖	mathematical	Finset.Nonempty padicNorm	padicNorm Finset.sum Rat.addCommMonoid	—	Finset.induction_on Finset.sum_insert LE.le.trans nonarchimedean max_le Finset.mem_insert_self Finset.mem_insert_of_mem Finset.sum_congr Finset.instLawfulSingleton Finset.sum_singleton
sum_le' 📖	mathematical	padicNorm	padicNorm Finset.sum Rat.addCommMonoid	—	Finset.eq_empty_or_nonempty zero sum_le
sum_lt 📖	mathematical	Finset.Nonempty padicNorm	padicNorm Finset.sum Rat.addCommMonoid	—	Finset.induction_on Finset.sum_insert lt_of_le_of_lt nonarchimedean max_lt Finset.mem_insert_self Finset.mem_insert_of_mem Finset.sum_congr Finset.instLawfulSingleton Finset.sum_singleton
sum_lt' 📖	mathematical	padicNorm	padicNorm Finset.sum Rat.addCommMonoid	—	Finset.eq_empty_or_nonempty zero sum_lt
triangle_ineq 📖	mathematical	—	padicNorm	—	nonarchimedean max_le_add_of_nonneg Rat.instAddLeftMono covariant_swap_add_of_covariant_add nonneg
values_discrete 📖	mathematical	—	padicNorm	—	zpow_neg
zero 📖	mathematical	—	padicNorm	—	—
zero_of_padicNorm_eq_zero 📖	—	padicNorm	—	—	by_contradiction zpow_ne_zero Nat.cast_zero Rat.instCharZero Nat.Prime.ne_zero Fact.out

---

← Back to Index