AdmissibleAbsoluteValue

📁 Source: Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean

Statistics

Metric	Count
Definitions IsAdmissible, card	2
Theorems exists_approx, exists_approx_aux, exists_partition, exists_partition', toIsEuclidean	5
Total	7

AbsoluteValue

Definitions

Name	Category	Theorems
IsAdmissible 📖	CompData	—

AbsoluteValue.IsAdmissible

Definitions

Name	Category	Theorems
card 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_approx 📖	mathematical	Real Real.instLT Real.instZero	Real.instIntCast DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing EuclideanDomain.instMod SubNegMonoid.toZSMul Real.instAddGroup	—	exists_approx_aux Equiv.symm_apply_apply
exists_approx_aux 📖	mathematical	Real Real.instLT Real.instZero	Real.instIntCast DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing EuclideanDomain.instMod SubNegMonoid.toZSMul Real.instAddGroup	—	pow_zero Nat.instCharZero Nat.instAtLeastTwoHAddOfNat exists_partition Finite.of_fintype Fintype.exists_lt_card_fiber_of_mul_lt_card Fintype.card_fin Fintype.card_congr' pow_succ' Finset.length_toList List.Nodup.getElem_inj_iff Finset.nodup_toList Finset.mem_filter Finset.mem_toList
exists_partition 📖	mathematical	Real Real.instLT Real.instZero	Real.instIntCast DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing EuclideanDomain.instMod SubNegMonoid.toZSMul Real.instAddGroup	—	Finite.exists_equiv_fin exists_partition' Equiv.symm_apply_apply
exists_partition' 📖	mathematical	Real Real.instLT Real.instZero	Real.instIntCast DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AbsoluteValue.funLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing EuclideanDomain.instMod SubNegMonoid.toZSMul Real.instAddGroup	—	—
toIsEuclidean 📖	mathematical	—	AbsoluteValue.IsEuclidean Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	—

---

← Back to Index