ValMinAbs

📁 Source: Mathlib/Data/ZMod/ValMinAbs.lean

Statistics

Metric	Count
Definitions valMinAbs	1
Theorems abs_valMinAbs_eq_abs_valMinAbs, coe_valMinAbs, eq_neg_of_valMinAbs_eq_neg_valMinAbs, injective_valMinAbs, natAbs_valMinAbs_add_le, natAbs_valMinAbs_eq_natAbs_valMinAbs, natAbs_valMinAbs_le, natAbs_valMinAbs_neg, natCast_natAbs_valMinAbs, prime_ne_zero, valMinAbs_def_pos, valMinAbs_def_zero, valMinAbs_eq_zero, valMinAbs_inj, valMinAbs_mem_Ioc, valMinAbs_mul_two_eq_iff, valMinAbs_natAbs_eq_min, valMinAbs_natCast_eq_self, valMinAbs_natCast_of_half_lt, valMinAbs_natCast_of_le_half, valMinAbs_neg_of_ne_half, valMinAbs_nonneg_iff, valMinAbs_spec, valMinAbs_zero, val_eq_ite_valMinAbs	25
Total	26

ZMod

Definitions

Name	Category	Theorems
valMinAbs 📖	CompOp	24 math math: injective_valMinAbs, natCast_natAbs_valMinAbs, valMinAbs_neg_of_ne_half, valMinAbs_def_pos, valMinAbs_mem_Ioc, valMinAbs_natCast_of_le_half, valMinAbs_natCast_of_half_lt, valMinAbs_nonneg_iff, valMinAbs_zero, natAbs_valMinAbs_eq_natAbs_valMinAbs, coe_valMinAbs, valMinAbs_natAbs_eq_min, valMinAbs_mul_two_eq_iff, valMinAbs_eq_zero, natAbs_valMinAbs_neg, val_eq_ite_valMinAbs, natAbs_valMinAbs_le, Ico_map_valMinAbs_natAbs_eq_Ico_map_id, abs_valMinAbs_eq_abs_valMinAbs, valMinAbs_natCast_eq_self, natAbs_valMinAbs_add_le, valMinAbs_def_zero, valMinAbs_inj, valMinAbs_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_valMinAbs_eq_abs_valMinAbs 📖	mathematical	—	abs instLatticeInt Int.instAddGroup valMinAbs ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	natAbs_valMinAbs_eq_natAbs_valMinAbs Int.abs_eq_natAbs Int.instCharZero
coe_valMinAbs 📖	mathematical	—	ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing commRing valMinAbs	—	valMinAbs_def_pos Int.cast_natCast natCast_zmod_val Int.cast_sub natCast_self sub_zero
eq_neg_of_valMinAbs_eq_neg_valMinAbs 📖	mathematical	valMinAbs	ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	eq_zero_or_neZero Int.cast_neg coe_valMinAbs neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
injective_valMinAbs 📖	mathematical	—	ZMod valMinAbs	—	Function.injective_iff_hasLeftInverse coe_valMinAbs
natAbs_valMinAbs_add_le 📖	mathematical	—	valMinAbs ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing	—	le_refl natAbs_min_of_le_div_two Int.cast_add coe_valMinAbs natAbs_valMinAbs_le
natAbs_valMinAbs_eq_natAbs_valMinAbs 📖	mathematical	—	valMinAbs ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	eq_neg_of_valMinAbs_eq_neg_valMinAbs natAbs_valMinAbs_neg
natAbs_valMinAbs_le 📖	mathematical	—	valMinAbs	—	Nat.le_div_two_iff_mul_two_le valMinAbs_mem_Ioc neg_le_neg_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add neg_mul LT.lt.le
natAbs_valMinAbs_neg 📖	mathematical	—	valMinAbs ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	neg_eq_self_iff valMinAbs_neg_of_ne_half
natCast_natAbs_valMinAbs 📖	mathematical	—	ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing valMinAbs val NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	sub_nonpos covariant_swap_add_of_covariant_add Int.instAddLeftMono val_le valMinAbs_def_pos natCast_zmod_val Int.cast_natCast Int.cast_neg Int.cast_sub natCast_self sub_zero
prime_ne_zero 📖	—	—	—	—	Nat.cast_zero natCast_eq_natCast_iff Nat.modEq_zero_iff_dvd Nat.Prime.coprime_iff_not_dvd Fact.out Nat.coprime_primes
valMinAbs_def_pos 📖	mathematical	—	valMinAbs val	—	—
valMinAbs_def_zero 📖	mathematical	—	valMinAbs	—	—
valMinAbs_eq_zero 📖	mathematical	—	valMinAbs ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing	—	injective_valMinAbs valMinAbs_zero
valMinAbs_inj 📖	mathematical	—	valMinAbs	—	injective_valMinAbs
valMinAbs_mem_Ioc 📖	mathematical	—	Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt valMinAbs	—	valMinAbs_def_pos LT.lt.trans_le neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono Nat.cast_zero Int.instZeroLEOneClass Int.instCharZero NeZero.pos Nat.instCanonicallyOrderedAdd mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Nat.cast_nonneg zero_le_two lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le le_trans mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono
valMinAbs_mul_two_eq_iff 📖	mathematical	—	valMinAbs val	—	CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instCharZero Nat.cast_mul Nat.cast_two mul_comm Nat.cast_one mul_nonneg_iff_left_nonneg_of_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono zero_lt_two Int.instZeroLEOneClass Int.instAddLeftMono valMinAbs_nonneg_iff Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Eq.le
valMinAbs_natAbs_eq_min 📖	mathematical	—	valMinAbs val	—	valMinAbs_def_pos val_lt
valMinAbs_natCast_eq_self 📖	mathematical	—	valMinAbs ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing	—	natAbs_valMinAbs_le valMinAbs_natCast_of_le_half
valMinAbs_natCast_of_half_lt 📖	mathematical	—	valMinAbs ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing	—	not_lt_bot valMinAbs_def_pos val_natCast LT.lt.not_ge Nat.cast_add Nat.cast_one
valMinAbs_natCast_of_le_half 📖	mathematical	—	valMinAbs ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing	—	valMinAbs_def_pos val_natCast LE.le.trans_lt Nat.div_lt_self'
valMinAbs_neg_of_ne_half 📖	mathematical	—	valMinAbs ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	eq_zero_or_neZero valMinAbs_spec Int.cast_neg coe_valMinAbs neg_mul neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add LE.le.lt_of_ne valMinAbs_mem_Ioc valMinAbs_mul_two_eq_iff le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le
valMinAbs_nonneg_iff 📖	mathematical	—	valMinAbs val	—	valMinAbs_def_pos Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing LT.lt.not_ge sub_lt_zero IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono val_lt
valMinAbs_spec 📖	mathematical	—	valMinAbs ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing commRing Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	coe_valMinAbs valMinAbs_mem_Ioc sub_eq_zero Int.eq_zero_of_abs_lt_dvd intCast_zmod_eq_zero_iff_dvd Int.cast_sub sub_self Nat.instAtLeastTwoHAddOfNat mul_lt_mul_iff_left₀ IsStrictOrderedRing.toMulPosStrictMono Int.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE zero_lt_two Int.instZeroLEOneClass Int.instAddLeftMono abs_eq_self Int.instIsOrderedAddMonoid zero_le_two abs_mul IsStrictOrderedRing.toIsOrderedRing sub_mul abs_lt covariant_swap_add_of_covariant_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le
valMinAbs_zero 📖	mathematical	—	valMinAbs ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing	—	valMinAbs_def_pos val_zero Nat.instCanonicallyOrderedAdd
val_eq_ite_valMinAbs 📖	mathematical	—	val valMinAbs	—	valMinAbs_def_pos natCast_val CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero add_zero sub_add_cancel

---

← Back to Index