SiegelsLemma

📁 Source: Mathlib/NumberTheory/SiegelsLemma.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_ne_zero_int_vec_norm_le, exists_ne_zero_int_vec_norm_le', one_le_norm_A_of_ne_zero	3
Total	3

Int.Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_ne_zero_int_vec_norm_le 📖	mathematical	Fintype.card	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real Real.instLE Norm.norm NormedRing.toNorm Pi.normedRing NormedCommRing.toNormedRing Real.instPow Real.instMul Real.instNatCast Real.instMax Real.instOne Matrix SeminormedAddCommGroup.toNorm Matrix.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub	—	Real.instIsStrictOrderedRing Finset.exists_ne_map_eq_of_card_lt_of_maps_to sub_ne_zero Matrix.mulVec_sub Real.rpow_nonneg mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass le_of_lt lt_max_of_lt_left Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Matrix.norm_replicateCol Matrix.norm_le_iff Int.norm_eq_abs Int.cast_abs le_trans Int.cast_natCast RCLike.charZero_rclike Rat.cast_divInt Int.cast_subNatNat NeZero.charZero_one abs_le Int.instIsOrderedAddMonoid Int.instAddLeftMono Finset.mem_Icc covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.floor_le
exists_ne_zero_int_vec_norm_le' 📖	mathematical	Fintype.card	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real Real.instLE Norm.norm NormedRing.toNorm Pi.normedRing NormedCommRing.toNormedRing Real.instPow Real.instMul Real.instNatCast Matrix SeminormedAddCommGroup.toNorm Matrix.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub	—	exists_ne_zero_int_vec_norm_le max_eq_right one_le_norm_A_of_ne_zero
one_le_norm_A_of_ne_zero 📖	mathematical	—	Real Real.instLE Real.instOne Norm.norm Matrix SeminormedAddCommGroup.toNorm Matrix.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Int.instNormedCommRing	—	Matrix.ext Int.abs_lt_one_iff Nat.cast_one Real.instIsStrictOrderedRing Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Int.norm_eq_abs Matrix.norm_lt_iff Real.zero_lt_one

---

← Back to Index