Documentation Verification Report

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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	`Finset` `AddSubgroup` `SetLike.instMembership` `instSetLike` `IsComplement` `toAddGroup` `SetLike.coe` `Finset.instSetLike` `addSubgroupOf` `Set.iUnion` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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`	—	`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` `SetLike.instMembership` `Finset.instSetLike` `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.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubgroup` `instSetLike` `Set.univ`	—	`leftCoset_cover_filter_FiniteIndex_aux`
`leftCoset_cover_filter_FiniteIndex_aux` 📖	mathematical	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `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.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `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`	—	`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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `AddSubgroup` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `AddSubgroup` `instSetLike`	—	`leftCoset_cover_filter_FiniteIndex_aux`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finiteIndex_of_leftCoset_cover` 📖	mathematical	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `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` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `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`	`Finset` `Subgroup` `SetLike.instMembership` `instSetLike` `IsComplement` `toGroup` `SetLike.coe` `Finset.instSetLike` `subgroupOf` `Set.iUnion` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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`	—	—
`leftCoset_cover_filter_FiniteIndex` 📖	mathematical	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	—	`leftCoset_cover_filter_FiniteIndex_aux`
`leftCoset_cover_filter_FiniteIndex_aux` 📖	mathematical	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `instSetLike` `Set.univ`	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `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`	—	`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` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Subgroup` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.filter` `FiniteIndex` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Subgroup` `instSetLike`	—	`leftCoset_cover_filter_FiniteIndex_aux`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finiteIndex_of_cover` 📖	mathematical	`Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `SetLike.coe` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setLike` `Set.univ`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `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` `SetLike.instMembership` `Finset.instSetLike` `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` `Subspace` `Submodule.instTop` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`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` `SetLike.instMembership` `Finset.instSetLike` `SetLike.coe` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set.univ`	`Subspace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Top.top` `Submodule.instTop` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `biUnion_ne_univ_of_top_notMem`

---

← Back to Index