Int

📁 Source: Mathlib/Algebra/Order/Ring/Int.lean

Statistics

Metric	Count
Definitions	0
Theorems add_two_le_iff_lt_of_even_sub, instIsStrictOrderedRing, isCompl_even_odd, two_le_iff_pos_of_even, cast_natAbs, exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le	6
Total	6

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_two_le_iff_lt_of_even_sub 📖	—	Even	—	—	—
instIsStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	IsStrictOrderedRing.of_mul_pos instIsOrderedAddMonoid instZeroLEOneClass instNontrivial
isCompl_even_odd 📖	mathematical	—	IsCompl Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra Set.instBoundedOrder setOf Even Odd instSemiring	—	—
two_le_iff_pos_of_even 📖	—	Even	—	—	le_iff_pos_of_dvd Even.two_dvd

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_natAbs 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast abs instLatticeInt Int.instAddGroup	—	Int.natCast_natAbs Int.cast_natCast
exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le 📖	—	—	—	—	MulZeroClass.mul_zero mul_comm zero_add add_zero Int.gcd_dvd_iff cast_injective Int.instCharZero add_mul Distrib.rightDistribClass add_assoc add_right_comm mul_right_comm cast_add cast_mul lt_irrefl add_le_add Int.instAddLeftMono covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing cast_succ mul_add Distrib.leftDistribClass sub_le_sub_iff_right cast_le Int.instZeroLEOneClass

---

← Back to Index