CardIntervalMod

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

Statistics

Metric	Count
Definitions	0
Theorems Ico_filter_dvd_card, Ico_filter_dvd_eq, Ico_filter_modEq_card, Ico_filter_modEq_eq, Ioc_filter_dvd_card, Ioc_filter_dvd_eq, Ioc_filter_modEq_card, Ioc_filter_modEq_eq, Ico_filter_modEq_card, Ico_filter_modEq_cast, Ioc_filter_modEq_card, Ioc_filter_modEq_cast, count_modEq_card, count_modEq_card_eq_ceil	14
Total	14

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ico_filter_dvd_card 📖	mathematical	—	Finset.card Finset.filter Finset.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' Ico_filter_dvd_eq Finset.card_map card_Ico
Ico_filter_dvd_eq 📖	mathematical	—	Finset.filter Finset.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder Finset.map mul_left_injective₀ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Finset.ext mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing cast_pos Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero
Ico_filter_modEq_card 📖	mathematical	—	Finset.card Finset.filter ModEq instDecidableModEq Finset.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd Ico_filter_modEq_eq Ico_filter_dvd_eq cast_sub Finset.card_map card_Ico
Ico_filter_modEq_eq 📖	mathematical	—	Finset.filter ModEq instDecidableModEq Finset.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder Finset.map add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid instAddGroup	—	Finset.ext add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono covariant_swap_add_of_covariant_add instAddLeftMono
Ioc_filter_dvd_card 📖	mathematical	—	Finset.card Finset.filter Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' Ioc_filter_dvd_eq Finset.card_map card_Ioc
Ioc_filter_dvd_eq 📖	mathematical	—	Finset.filter Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder Finset.map mul_left_injective₀ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Finset.ext mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing cast_pos Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero
Ioc_filter_modEq_card 📖	mathematical	—	Finset.card Finset.filter ModEq instDecidableModEq Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero LT.lt.ne' add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd Ioc_filter_modEq_eq Ioc_filter_dvd_eq cast_sub Finset.card_map card_Ioc
Ioc_filter_modEq_eq 📖	mathematical	—	Finset.filter ModEq instDecidableModEq Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instLocallyFiniteOrder Finset.map add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid instAddGroup	—	Finset.ext add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono covariant_swap_add_of_covariant_add instAddLeftMono

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ico_filter_modEq_card 📖	mathematical	—	Finset.card Finset.filter ModEq instDecidableModEq Finset.Ico instPreorder instLocallyFiniteOrder Int.ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Int.instCharZero Finset.card_map Ico_filter_modEq_cast Int.Ico_filter_modEq_card cast_lt Int.instAddLeftMono Int.instZeroLEOneClass Int.cast_natCast
Ico_filter_modEq_cast 📖	mathematical	—	Finset.map castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Int.instCharZero Finset.filter ModEq instDecidableModEq Finset.Ico instPreorder instLocallyFiniteOrder Int.ModEq Int.instDecidableModEq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder	—	Finset.ext Int.instCharZero Int.instAddLeftMono Int.instZeroLEOneClass CanLift.prf instCanLiftIntNatCastLeOfNat
Ioc_filter_modEq_card 📖	mathematical	—	Finset.card Finset.filter ModEq instDecidableModEq Finset.Ioc instPreorder instLocallyFiniteOrder Int.floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Int.instCharZero Finset.card_map Ioc_filter_modEq_cast Int.Ioc_filter_modEq_card cast_lt Int.instAddLeftMono Int.instZeroLEOneClass Int.cast_natCast
Ioc_filter_modEq_cast 📖	mathematical	—	Finset.map castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Int.instCharZero Finset.filter ModEq instDecidableModEq Finset.Ioc instPreorder instLocallyFiniteOrder Int.ModEq Int.instDecidableModEq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Int.instLocallyFiniteOrder	—	Finset.ext Int.instCharZero Int.instAddLeftMono Int.instZeroLEOneClass CanLift.prf instCanLiftIntNatCastLeOfNat
count_modEq_card 📖	mathematical	—	count ModEq instDecidableModEq	—	cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero count_modEq_card_eq_ceil cast_add cast_mul add_sub add_div mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass LT.lt.ne' add_comm Int.ceil_add_natCast Rat.instIsStrictOrderedRing AddLeftCancelSemigroup.toIsLeftCancelAdd cast_sub LT.lt.le Int.ceil_eq_iff div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono lt_div_iff₀ cast_one Int.cast_one sub_self MulZeroClass.zero_mul cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial tsub_pos_iff_lt instCanonicallyOrderedAdd instOrderedSub one_mul cast_le tsub_le_iff_right LT.lt.trans_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le cast_zero Int.ceil_eq_zero_iff Set.mem_Ioc tsub_nonpos AddGroup.toOrderedSub covariant_swap_add_of_covariant_add neg_eq_neg_one_mul neg_lt_sub_iff_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd cast_lt not_lt
count_modEq_card_eq_ceil 📖	mathematical	—	count ModEq instDecidableModEq Int.ceil DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero count_eq_card_filter_range Ico_zero_eq_range Ico_filter_modEq_card max_eq_left sub_nonneg covariant_swap_add_of_covariant_add Int.instAddLeftMono Int.ceil_le_ceil div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing sub_le_sub_right mono_cast zero_le instCanonicallyOrderedAdd le_of_lt cast_add cast_mul add_comm sub_div mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass LT.lt.ne' Int.ceil_sub_natCast sub_sub_sub_cancel_right cast_zero zero_sub sub_eq_self Int.ceil_eq_zero_iff Set.mem_Ioc div_le_iff₀ lt_div_iff₀ neg_one_mul MulZeroClass.zero_mul neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd cast_lt IsStrictOrderedRing.toIsOrderedRing

---

← Back to Index