Lemmas

📁 Source: Mathlib/Data/Int/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems div2_bit, ediv_emod_unique'', injOn_natAbs_Ici, injOn_natAbs_Iic, le_natCast_sub, natAbs_coe_sub_coe_le_of_le, natAbs_coe_sub_coe_lt_of_lt, natAbs_eq_iff_sq_eq, natAbs_inj_of_nonneg_of_nonneg, natAbs_inj_of_nonneg_of_nonpos, natAbs_inj_of_nonpos_of_nonneg, natAbs_inj_of_nonpos_of_nonpos, natAbs_le_iff_sq_le, natAbs_lt_iff_sq_lt, strictAntiOn_natAbs, strictMonoOn_natAbs, succ_natCast_pos	17
Total	17

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div2_bit 📖	mathematical	—	div2 bit	—	bit_val div2_val add_comm Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.cast_zero zero_add
ediv_emod_unique'' 📖	mathematical	—	abs instLatticeInt instAddGroup	—	emod_lt_abs ediv_eq_zero_of_lt_abs zero_add emod_abs
injOn_natAbs_Ici 📖	mathematical	—	Set.InjOn Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	StrictMonoOn.injOn strictMonoOn_natAbs
injOn_natAbs_Iic 📖	mathematical	—	Set.InjOn Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	StrictAntiOn.injOn strictAntiOn_natAbs
le_natCast_sub 📖	—	—	—	—	—
natAbs_coe_sub_coe_le_of_le 📖	—	—	—	—	Nat.cast_le instAddLeftMono instZeroLEOneClass instCharZero natCast_natAbs abs_sub_le_of_nonneg_of_le instIsOrderedAddMonoid
natAbs_coe_sub_coe_lt_of_lt 📖	—	—	—	—	Nat.cast_lt instAddLeftMono instZeroLEOneClass instCharZero natCast_natAbs abs_sub_lt_of_nonneg_of_lt instIsOrderedAddMonoid
natAbs_eq_iff_sq_eq 📖	mathematical	—	Monoid.toNatPow instMonoid	—	sq natAbs_eq_iff_mul_self_eq
natAbs_inj_of_nonneg_of_nonneg 📖	—	—	—	—	sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing natAbs_eq_iff_sq_eq
natAbs_inj_of_nonneg_of_nonpos 📖	—	—	—	—	natAbs_inj_of_nonneg_of_nonneg neg_nonneg_of_nonpos instIsOrderedAddMonoid
natAbs_inj_of_nonpos_of_nonneg 📖	—	—	—	—	natAbs_inj_of_nonneg_of_nonneg neg_nonneg_of_nonpos instIsOrderedAddMonoid
natAbs_inj_of_nonpos_of_nonpos 📖	—	—	—	—	natAbs_inj_of_nonneg_of_nonneg neg_nonneg_of_nonpos instIsOrderedAddMonoid
natAbs_le_iff_sq_le 📖	mathematical	—	Monoid.toNatPow instMonoid	—	sq natAbs_le_iff_mul_self_le
natAbs_lt_iff_sq_lt 📖	mathematical	—	Monoid.toNatPow instMonoid	—	sq natAbs_lt_iff_mul_self_lt
strictAntiOn_natAbs 📖	mathematical	—	StrictAntiOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Nat.instPreorder Set.Iic	—	Right.nonneg_neg_iff covariant_swap_add_of_covariant_add instAddLeftMono neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
strictMonoOn_natAbs 📖	mathematical	—	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Nat.instPreorder Set.Ici	—	—
succ_natCast_pos 📖	—	—	—	—	IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing

---

← Back to Index