AdmissibleAbs

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

Statistics

Metric	Count
Definitions absIsAdmissible, instInhabitedIsAdmissibleIntAbs	2
Theorems exists_partition_int	1
Total	3

AbsoluteValue

Definitions

Name	Category	Theorems
absIsAdmissible 📖	CompOp	—
instInhabitedIsAdmissibleIntAbs 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_partition_int 📖	mathematical	Real Real.instLT Real.instZero	Real.instIntCast abs instLatticeInt Int.instAddGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Real.instAddGroup	—	Int.cast_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing abs_pos Int.instAddLeftMono Algebra.smul_def mul_pos IsStrictOrderedRing.toPosMulStrictMono Int.floor_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Int.cast_nonneg LT.lt.le Int.floor_lt eq_intCast RingHom.instRingHomClass div_div lt_of_lt_of_le div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_lt_one Int.cast_lt Int.emod_lt_abs Nat.le_ceil Int.abs_sub_lt_one_of_floor_eq_floor Int.cast_abs Int.cast_sub one_mul div_lt_iff₀ abs_of_nonneg abs_div sub_div abs_sub_comm

---

← Back to Index