CosetCover

📁 Source: Mathlib/GroupTheory/CosetCover.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_finiteIndex_of_leftCoset_cover, exists_finiteIndex_of_leftCoset_cover_aux, exists_index_le_card_of_leftCoset_cover, exists_leftTransversal_of_FiniteIndex, finiteIndex_of_leftCoset_cover_const, index_le_of_leftCoset_cover_const, leftCoset_cover_const_iff_surjOn, leftCoset_cover_filter_FiniteIndex, leftCoset_cover_filter_FiniteIndex_aux, one_le_sum_inv_index_of_leftCoset_cover, pairwiseDisjoint_leftCoset_cover_const_of_index_eq, pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, exists_finiteIndex_of_leftCoset_cover, exists_finiteIndex_of_leftCoset_cover_aux, exists_index_le_card_of_leftCoset_cover, exists_leftTransversal_of_FiniteIndex, finiteIndex_of_leftCoset_cover_const, index_le_of_leftCoset_cover_const, leftCoset_cover_const_iff_surjOn, leftCoset_cover_filter_FiniteIndex, leftCoset_cover_filter_FiniteIndex_aux, one_le_sum_inv_index_of_leftCoset_cover, pairwiseDisjoint_leftCoset_cover_const_of_index_eq, pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, exists_finiteIndex_of_cover, biUnion_ne_univ_of_top_notMem, exists_eq_top_of_iUnion_eq_univ, top_mem_of_biUnion_eq_univ	28
Total	28

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finiteIndex_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	FiniteIndex	—	Set.empty_ne_univ Zero.instNonempty Set.biUnion_empty Finset.coe_empty Finset.set_biUnion_coe Finset.not_nonempty_iff_eq_empty finiteIndex_of_leftCoset_cover_const Set.iUnion₂_congr Finset.mem_filter exists_finiteIndex_of_leftCoset_cover_aux
exists_finiteIndex_of_leftCoset_cover_aux 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	FiniteIndex	—	Set.iUnion_congr_Prop Finset.mem_filter Set.eq_univ_iff_forall Set.mem_iUnion mem_leftAddCoset_iff SetLike.mem_coe QuotientAddGroup.eq neg_add_cancel_left add_assoc neg_add_rev neg_neg Finset.mem_erase Finset.mem_image_of_mem Set.iUnion₂_eq_univ_iff Set.mem_union Eq.superset Set.instReflSubset Finset.set_biUnion_union Finset.filter_union_filter_not_eq Set.mem_univ Set.mem_iUnion₂ Finset.mem_univ not_isEmpty_iff Set.empty_ne_univ Zero.instNonempty Set.iUnion_of_empty Finset.mem_of_mem_filter finiteIndex_of_leftCoset_cover_const Set.iUnion₂_congr LE.le.trans_lt Finset.card_le_card mem_image_univ_iff_mem_range Set.mem_range Finset.card_erase_lt_of_mem
exists_index_le_card_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	FiniteIndex index Finset.card	—	LE.le.not_gt one_le_sum_inv_index_of_leftCoset_cover Finset.eq_empty_or_nonempty Finset.sum_congr zero_lt_one Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero Finset.Nonempty.card_pos eq_or_ne Nat.cast_zero inv_zero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial inv_strictAnti₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_lt Rat.instAddLeftMono Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq not_le LT.lt.trans_eq Finset.sum_lt_sum_of_nonempty IsStrictOrderedRing.toIsOrderedCancelAddMonoid Finset.sum_const nsmul_eq_mul mul_inv_cancel₀ Nat.cast_ne_zero LT.lt.ne'
exists_leftTransversal_of_FiniteIndex 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	IsComplement SetLike.instMembership instSetLike toAddGroup SetLike.coe Finset Finset.instSetLike addSubgroupOf Set.iUnion Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	exists_isComplement_left IsComplement.finite_left_iff instFiniteIndex_addSubgroupOf Set.Finite.coe_toFinset Set.ext add_mem IsComplement.neg_toLeftFun_add_mem add_neg_cancel_left Set.iUnion_congr_Prop Set.Finite.mem_toFinset Set.mem_iUnion SetLike.mem_coe
finiteIndex_of_leftCoset_cover_const 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	FiniteIndex	—	Set.finite_univ_iff Set.Finite.of_surjOn leftCoset_cover_const_iff_surjOn Finset.finite_toSet finiteIndex_of_finite_quotient
index_le_of_leftCoset_cover_const 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	index Finset.card	—	LE.le.trans_eq Nat.card_le_card_of_surjective Finite.of_fintype Set.surjOn_iff_surjective leftCoset_cover_const_iff_surjOn Nat.card_eq_finsetCard
leftCoset_cover_const_iff_surjOn 📖	mathematical	—	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ Set.SurjOn HasQuotient.Quotient QuotientAddGroup.instHasQuotientAddSubgroup Finset.instSetLike	—	Set.eq_univ_iff_forall Set.mem_iUnion mem_leftAddCoset_iff SetLike.mem_coe Set.univ_subset_iff Set.mem_image QuotientAddGroup.eq
leftCoset_cover_filter_FiniteIndex 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	Finset.filter FiniteIndex	—	leftCoset_cover_filter_FiniteIndex_aux
leftCoset_cover_filter_FiniteIndex_aux 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	Finset.filter FiniteIndex Finset.sum Rat.addCommMonoid index Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike	—	finiteIndex_iInf' Finset.mem_filter iInf₂_le Finset.filter_union_filter_not_eq Finset.set_biUnion_union Set.iUnion_sigma Set.iUnion_subtype Set.iUnion_congr Set.iUnion_congr_Prop Finset.mem_univ leftAddCoset_assoc Set.iUnion_true Set.vadd_set_iUnion₂ vadd_coe_set instAddSubgroupClass SetLike.coe_mem Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Finset.mem_singleton Set.iUnion_iUnion_eq_left add_zero exists_finiteIndex_of_leftCoset_cover Finset.nonempty_coe_sort Equiv.nonempty Set.iUnion₂_congr exists_finiteIndex_of_leftCoset_cover_aux eq_mul_inv_iff_mul_eq₀ Nat.cast_ne_zero Rat.instCharZero FiniteIndex.index_ne_zero Finset.sum_mul Finset.sum_attach Finset.card_filter Nat.cast_sum Finset.univ_sigma_univ Finset.sum_sigma Finset.sum_coe_sort_eq_attach Finset.sum_congr relIndex_mul_index Nat.cast_mul mul_comm mul_inv_cancel_right₀ Nat.cast_one Finset.sum_const Finset.card_attach nsmul_eq_mul mul_one Nat.card_eq_fintype_card Fintype.card_coe IsComplement.card_left of_not_not Function.mt Nat.cast_zero inv_zero MulZeroClass.zero_mul Nat.cast_ite Finset.sum_ite_irrel Finset.card_singleton one_smul Finset.sum_const_zero one_ne_zero NeZero.charZero_one Set.iUnion_and Set.vadd_set_iUnion Finset.filter.congr_simp IsEmpty.forall_iff le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing one_mul mul_assoc inv_mul_cancel₀ Nat.cast_le Rat.instAddLeftMono Rat.instZeroLEOneClass index_le_of_leftCoset_cover_const Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial mul_inv_eq_one₀ Finset.coe_filter pairwiseDisjoint_leftCoset_cover_const_of_index_eq Set.mem_vadd_set_iff_neg_vadd_mem neg_add_rev add_assoc SetLike.mem_coe Set.mem_iUnion Set.mem_setOf_eq Set.singleton_subset_iff Set.le_iff_subset exists_leftTransversal_of_FiniteIndex
one_le_sum_inv_index_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ	Finset.sum Rat.addCommMonoid index	—	leftCoset_cover_filter_FiniteIndex_aux
pairwiseDisjoint_leftCoset_cover_const_of_index_eq 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ index Finset.card	Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike	—	Set.empty_ne_univ Zero.instNonempty Set.biUnion_empty Finset.coe_empty Finset.set_biUnion_coe Finset.card_eq_zero Fintype.bijective_iff_surjective_and_card Set.surjOn_iff_surjective leftCoset_cover_const_iff_surjOn Fintype.card_coe Nat.card_eq_fintype_card Function.Bijective.injective QuotientAddGroup.eq SetLike.mem_coe mem_leftAddCoset_iff
pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero 📖	mathematical	Set.iUnion Finset Finset.instMembership HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup instSetLike Set.univ Finset.sum Rat.addCommMonoid index	Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike Finset.filter FiniteIndex	—	leftCoset_cover_filter_FiniteIndex_aux

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finiteIndex_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	FiniteIndex	—	Set.empty_ne_univ One.instNonempty Set.biUnion_empty Finset.coe_empty Finset.set_biUnion_coe finiteIndex_of_leftCoset_cover_const Set.iUnion₂_congr Finset.mem_filter exists_finiteIndex_of_leftCoset_cover_aux
exists_finiteIndex_of_leftCoset_cover_aux 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	FiniteIndex	—	Set.iUnion_congr_Prop Set.eq_univ_iff_forall QuotientGroup.eq SetLike.mem_coe mem_leftCoset_iff inv_mul_cancel_left mul_assoc mul_inv_rev inv_inv Finset.mem_filter Finset.mem_erase Finset.mem_image_of_mem Set.iUnion₂_eq_univ_iff Set.mem_union Eq.superset Set.instReflSubset Finset.set_biUnion_union Finset.filter_union_filter_not_eq Set.mem_univ Set.mem_iUnion₂ Finset.mem_univ not_isEmpty_iff Set.empty_ne_univ One.instNonempty Set.iUnion_of_empty Finset.mem_of_mem_filter finiteIndex_of_leftCoset_cover_const Set.iUnion₂_congr LE.le.trans_lt Finset.card_le_card mem_image_univ_iff_mem_range Set.mem_range Finset.card_erase_lt_of_mem
exists_index_le_card_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	FiniteIndex index Finset.card	—	LE.le.not_gt one_le_sum_inv_index_of_leftCoset_cover Finset.eq_empty_or_nonempty Finset.sum_congr Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero Finset.Nonempty.card_pos eq_or_ne Nat.cast_zero inv_zero inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial inv_strictAnti₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instAddLeftMono Mathlib.Tactic.Push.not_and_eq LT.lt.trans_eq Finset.sum_lt_sum_of_nonempty IsStrictOrderedRing.toIsOrderedCancelAddMonoid Finset.sum_const nsmul_eq_mul mul_inv_cancel₀ Nat.cast_ne_zero LT.lt.ne'
exists_leftTransversal_of_FiniteIndex 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	IsComplement SetLike.instMembership instSetLike toGroup SetLike.coe Finset Finset.instSetLike subgroupOf Set.iUnion Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	exists_isComplement_left IsComplement.finite_left_iff instFiniteIndex_subgroupOf Set.Finite.coe_toFinset Set.ext mul_mem IsComplement.inv_toLeftFun_mul_mem mul_inv_cancel_left Set.iUnion_congr_Prop
finiteIndex_of_leftCoset_cover_const 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	FiniteIndex	—	Set.finite_univ_iff Set.Finite.of_surjOn Finset.finite_toSet finiteIndex_of_finite_quotient
index_le_of_leftCoset_cover_const 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	index Finset.card	—	LE.le.trans_eq Nat.card_le_card_of_surjective Finite.of_fintype Set.surjOn_iff_surjective leftCoset_cover_const_iff_surjOn Nat.card_eq_finsetCard
leftCoset_cover_const_iff_surjOn 📖	mathematical	—	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ Set.SurjOn HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup Finset.instSetLike	—	—
leftCoset_cover_filter_FiniteIndex 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	Finset.filter FiniteIndex	—	leftCoset_cover_filter_FiniteIndex_aux
leftCoset_cover_filter_FiniteIndex_aux 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	Finset.filter FiniteIndex Finset.sum Rat.addCommMonoid index Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike	—	finiteIndex_iInf' iInf₂_le Finset.mem_filter Finset.filter_union_filter_not_eq Finset.set_biUnion_union Set.iUnion_sigma Set.iUnion_subtype Set.iUnion_congr Set.iUnion_congr_Prop Set.iUnion_true smul_coe_set instSubgroupClass Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.iUnion_iUnion_eq_left mul_one exists_finiteIndex_of_leftCoset_cover Finset.nonempty_coe_sort Equiv.nonempty Set.iUnion₂_congr exists_finiteIndex_of_leftCoset_cover_aux Finset.mem_univ eq_mul_inv_iff_mul_eq₀ Nat.cast_ne_zero Rat.instCharZero FiniteIndex.index_ne_zero Finset.sum_mul Finset.sum_attach Finset.card_filter Nat.cast_sum Finset.univ_sigma_univ Finset.sum_sigma Finset.sum_coe_sort_eq_attach Finset.sum_congr relIndex_mul_index Nat.cast_mul mul_comm mul_inv_cancel_right₀ Nat.cast_one Finset.sum_const Finset.card_attach nsmul_eq_mul Nat.card_eq_fintype_card Fintype.card_coe IsComplement.card_left of_not_not Function.mt Nat.cast_zero inv_zero MulZeroClass.zero_mul Nat.cast_ite Finset.sum_ite_irrel Finset.card_singleton one_smul Finset.sum_const_zero NeZero.charZero_one Set.iUnion_and Set.smul_set_iUnion Finset.filter.congr_simp le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing one_mul mul_assoc inv_mul_cancel₀ Nat.cast_le Rat.instAddLeftMono Rat.instZeroLEOneClass index_le_of_leftCoset_cover_const Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial mul_inv_eq_one₀ Finset.coe_filter pairwiseDisjoint_leftCoset_cover_const_of_index_eq mul_inv_rev Set.mem_setOf_eq Set.singleton_subset_iff Set.le_iff_subset exists_leftTransversal_of_FiniteIndex
one_le_sum_inv_index_of_leftCoset_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ	Finset.sum Rat.addCommMonoid index	—	leftCoset_cover_filter_FiniteIndex_aux
pairwiseDisjoint_leftCoset_cover_const_of_index_eq 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ index Finset.card	Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike	—	Set.empty_ne_univ One.instNonempty Set.biUnion_empty Finset.coe_empty Finset.set_biUnion_coe Finset.card_eq_zero Fintype.bijective_iff_surjective_and_card Set.surjOn_iff_surjective leftCoset_cover_const_iff_surjOn Fintype.card_coe Nat.card_eq_fintype_card Function.Bijective.injective QuotientGroup.eq SetLike.mem_coe mem_leftCoset_iff
pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one 📖	mathematical	Set.iUnion Finset Finset.instMembership Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup instSetLike Set.univ Finset.sum Rat.addCommMonoid index	Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Finset.instSetLike Finset.filter FiniteIndex	—	leftCoset_cover_filter_FiniteIndex_aux

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finiteIndex_of_cover 📖	mathematical	Set.iUnion Finset Finset.instMembership SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike Set.univ	AddSubgroup.FiniteIndex AddCommGroup.toAddGroup toAddSubgroup	—	Set.iUnion_congr_Prop zero_vadd AddSubgroup.exists_finiteIndex_of_leftCoset_cover

Subspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_ne_univ_of_top_notMem 📖	—	Subspace Finset Finset.instMembership Top.top Submodule.instTop DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	—	Submodule.exists_finiteIndex_of_cover AddSubgroup.finite_quotient_of_finiteIndex Submodule.Quotient.nontrivial_iff Module.Free.infinite Module.Free.of_divisionRing not_finite
exists_eq_top_of_iUnion_eq_univ 📖	mathematical	Set.iUnion SetLike.coe Subspace Submodule.setLike DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set.univ	Top.top Submodule.instTop	—	Finite.Set.finite_range Set.mem_toFinset top_mem_of_biUnion_eq_univ Set.iUnion_congr_Prop Set.biUnion_range
top_mem_of_biUnion_eq_univ 📖	mathematical	Set.iUnion Subspace Finset Finset.instMembership SetLike.coe Submodule.setLike DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set.univ	Top.top Submodule.instTop	—	Mathlib.Tactic.Contrapose.contrapose₁ biUnion_ne_univ_of_top_notMem

---

← Back to Index