Int

📁 Source: Mathlib/Algebra/Order/Group/Unbundled/Int.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_ediv_le_abs, abs_eq_natAbs, abs_le_one_iff, abs_lt_one_iff, abs_natCast, abs_sign_of_ne_zero, abs_sign_of_nonzero, abs_sub_lt_of_lt_lt, ediv_eq_zero_of_lt_abs, emod_abs, emod_lt_abs, eq_zero_of_abs_lt_dvd, le_self_pow_two, le_self_sq, natAbs_abs, natAbs_le_self_pow_two, natAbs_le_self_sq, natAbs_sub_ne_zero_iff, natAbs_sub_pos_iff, natCast_natAbs, natCast_strictMono, one_le_abs, sign_eq_abs_ediv, sign_eq_ediv_abs', sign_mul_abs, sign_mul_self_eq_abs, abs_zsmul_eq_zero, zpow_abs_eq_one	28
Total	28

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_ediv_le_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_eq_natAbs ofNat_le_ofNat_of_le abs_neg
abs_eq_natAbs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_of_nonneg instAddLeftMono abs_of_nonpos le_of_lt
abs_le_one_iff 📖	mathematical	—	abs instLatticeInt instAddGroup	—	—
abs_lt_one_iff 📖	mathematical	—	abs instLatticeInt instAddGroup	—	—
abs_natCast 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_of_nonneg instAddLeftMono
abs_sign_of_ne_zero 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_eq_natAbs
abs_sign_of_nonzero 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_sign_of_ne_zero
abs_sub_lt_of_lt_lt 📖	mathematical	—	abs instLatticeInt instAddGroup	—	—
ediv_eq_zero_of_lt_abs 📖	—	abs instLatticeInt instAddGroup	—	—	abs_eq_natAbs neg_injective
emod_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_by_cases
emod_lt_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	emod_abs abs_pos instAddLeftMono
eq_zero_of_abs_lt_dvd 📖	—	abs instLatticeInt instAddGroup	—	—	natAbs_le_of_dvd_ne_zero abs_eq_natAbs
le_self_pow_two 📖	mathematical	—	Monoid.toNatPow instMonoid	—	le_self_sq
le_self_sq 📖	mathematical	—	Monoid.toNatPow instMonoid	—	le_trans natAbs_le_self_sq
natAbs_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	—
natAbs_le_self_pow_two 📖	mathematical	—	Monoid.toNatPow instMonoid	—	natAbs_le_self_sq
natAbs_le_self_sq 📖	mathematical	—	Monoid.toNatPow instMonoid	—	natAbs_sq sq
natAbs_sub_ne_zero_iff 📖	—	—	—	—	natAbs_sub_pos_iff
natAbs_sub_pos_iff 📖	—	—	—	—	—
natCast_natAbs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_eq_natAbs
natCast_strictMono 📖	mathematical	—	StrictMono Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	—
one_le_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_pos instAddLeftMono
sign_eq_abs_ediv 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_zero instAddLeftMono sign_mul_self_eq_abs
sign_eq_ediv_abs' 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_zero instAddLeftMono abs_eq_zero covariant_swap_add_of_covariant_add sign_mul_abs
sign_mul_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_eq_natAbs
sign_mul_self_eq_abs 📖	mathematical	—	abs instLatticeInt instAddGroup	—	abs_eq_natAbs sign_mul_self_eq_natAbs

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_zsmul_eq_zero 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid abs instLatticeInt Int.instAddGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Int.natCast_natAbs natCast_zsmul natAbs_nsmul_eq_zero
zpow_abs_eq_one 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid abs instLatticeInt Int.instAddGroup InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Int.natCast_natAbs zpow_natCast pow_natAbs_eq_one

---

← Back to Index