Blocks

📁 Source: Mathlib/GroupTheory/GroupAction/Blocks.lean

Statistics

Metric	Count
Definitions `BlockMem`, `instBoundedOrder`, `IsBlock`, `IsBlockSystem`, `IsFixedBlock`, `IsInvariantBlock`, `IsTrivialBlock`, `block_stabilizerOrderIso`, `BlockMem`, `instBoundedOrder`, `IsBlock`, `IsBlockSystem`, `IsFixedBlock`, `IsInvariantBlock`, `IsTrivialBlock`, `block_stabilizerOrderIso`	16
Theorems `coe_bot`, `coe_top`, `instNontrivial`, `addSubgroup`, `disjoint_vadd_left`, `disjoint_vadd_of_ne`, `disjoint_vadd_right`, `disjoint_vadd_set_vadd`, `disjoint_vadd_vadd_set`, `empty`, `eq_univ_of_card_lt`, `iInter`, `image`, `inter`, `isBlockSystem`, `ncard_block_add_ncard_orbit_eq`, `ncard_block_eq_relIndex`, `ncard_dvd_card`, `not_vadd_set_ssubset_vadd_set`, `of_addSubgroup_of_conjugate`, `of_orbit`, `of_subset`, `of_subsingleton`, `orbit`, `orbit_of_normal`, `orbit_stabilizer_eq`, `pairwiseDisjoint_range_vadd`, `preimage`, `singleton`, `stabilizer_le`, `subsingleton_of_card_lt`, `subtype_val_preimage`, `translate`, `univ`, `vadd_eq_of_mem`, `vadd_eq_of_nonempty`, `vadd_eq_or_disjoint`, `vadd_eq_vadd_of_nonempty`, `vadd_eq_vadd_of_subset`, `vadd_eq_vadd_or_disjoint`, `of_normal`, `isBlock`, `isInvariantBlock`, `orbit`, `univ`, `isBlock`, `isFixedBlock`, `of_orbits`, `image`, `isBlock`, `preimage`, `vadd`, `vadd_iff`, `isBlock_addSubgroup`, `isBlock_addSubgroup'`, `isBlock_iff_disjoint_vadd_of_ne`, `isBlock_iff_pairwiseDisjoint_range_vadd`, `isBlock_iff_vadd_eq_of_mem`, `isBlock_iff_vadd_eq_of_nonempty`, `isBlock_iff_vadd_eq_or_disjoint`, `isBlock_iff_vadd_eq_vadd_of_nonempty`, `isBlock_iff_vadd_eq_vadd_or_disjoint`, `isBlock_subtypeVal`, `isBlock_top`, `isInvariantBlock_iff_isFixedBlock`, `eq_or_disjoint`, `pairwiseDisjoint`, `stabilizer_orbit_eq`, `vadd_orbit_eq_orbit_vadd`, `coe_bot`, `coe_top`, `instNontrivial`, `disjoint_smul_left`, `disjoint_smul_of_ne`, `disjoint_smul_right`, `disjoint_smul_set_smul`, `disjoint_smul_smul_set`, `empty`, `eq_univ_of_card_lt`, `iInter`, `image`, `inter`, `isBlockSystem`, `ncard_block_eq_relIndex`, `ncard_block_mul_ncard_orbit_eq`, `ncard_dvd_card`, `not_smul_set_ssubset_smul_set`, `of_orbit`, `of_subgroup_of_conjugate`, `of_subset`, `of_subsingleton`, `orbit`, `orbit_of_normal`, `orbit_stabilizer_eq`, `pairwiseDisjoint_range_smul`, `preimage`, `singleton`, `smul_eq_of_mem`, `smul_eq_of_nonempty`, `smul_eq_or_disjoint`, `smul_eq_smul_of_nonempty`, `smul_eq_smul_of_subset`, `smul_eq_smul_or_disjoint`, `stabilizer_le`, `subgroup`, `subsingleton_of_card_lt`, `subtype_val_preimage`, `translate`, `univ`, `of_normal`, `isBlock`, `isInvariantBlock`, `orbit`, `univ`, `isBlock`, `isFixedBlock`, `of_orbits`, `image`, `isBlock`, `preimage`, `smul`, `smul_iff`, `isBlock_iff_disjoint_smul_of_ne`, `isBlock_iff_pairwiseDisjoint_range_smul`, `isBlock_iff_smul_eq_of_mem`, `isBlock_iff_smul_eq_of_nonempty`, `isBlock_iff_smul_eq_or_disjoint`, `isBlock_iff_smul_eq_smul_of_nonempty`, `isBlock_iff_smul_eq_smul_or_disjoint`, `isBlock_subgroup`, `isBlock_subgroup'`, `isBlock_subtypeVal`, `isBlock_top`, `isInvariantBlock_iff_isFixedBlock`, `eq_or_disjoint`, `pairwiseDisjoint`, `smul_orbit_eq_orbit_smul`, `stabilizer_orbit_eq`	138
Total	154

AddAction

Definitions

Name	Category	Theorems
`BlockMem` 📖	CompOp	4 math math: `BlockMem.coe_top`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `BlockMem.coe_bot`, `BlockMem.instNontrivial`
`IsBlock` 📖	MathDef	25 math math: `IsBlock.of_orbit`, `isBlock_iff_vadd_eq_vadd_of_nonempty`, `isBlock_iff_vadd_eq_of_nonempty`, `IsBlock.singleton`, `IsBlock.of_subset`, `isBlock_iff_vadd_eq_or_disjoint`, `IsFixedBlock.isBlock`, `IsTrivialBlock.isBlock`, `IsBlock.empty`, `isBlock_top`, `IsBlock.orbit`, `isBlock_iff_disjoint_vadd_of_ne`, `isBlock_iff_pairwiseDisjoint_range_vadd`, `isBlock_iff_vadd_eq_vadd_or_disjoint`, `BlockMem.coe_top`, `IsInvariantBlock.isBlock`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `isBlock_addSubgroup`, `BlockMem.coe_bot`, `IsBlock.of_subsingleton`, `IsBlock.univ`, `isBlock_addSubgroup'`, `isBlock_iff_vadd_eq_of_mem`, `isBlock_subtypeVal`, `IsBlock.orbit_of_normal`
`IsBlockSystem` 📖	MathDef	2 math math: `IsBlock.isBlockSystem`, `IsBlockSystem.of_normal`
`IsFixedBlock` 📖	MathDef	4 math math: `IsInvariantBlock.isFixedBlock`, `isInvariantBlock_iff_isFixedBlock`, `IsFixedBlock.orbit`, `IsFixedBlock.univ`
`IsInvariantBlock` 📖	MathDef	2 math math: `isInvariantBlock_iff_isFixedBlock`, `IsFixedBlock.isInvariantBlock`
`IsTrivialBlock` 📖	MathDef	2 math math: `IsTrivialBlock.vadd_iff`, `IsPreprimitive.isTrivialBlock_of_isBlock`
`block_stabilizerOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock_addSubgroup` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SetLike.coe`	—	`Set.disjoint_left` `vadd_coe_set` `vadd_assoc` `Set.vaddAssocClass`
`isBlock_addSubgroup'` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SetLike.coe`	—	`Set.disjoint_left` `op_vadd_coe_set` `vadd_assoc` `Set.vaddAssocClass` `AddOpposite.op_vadd`
`isBlock_iff_disjoint_vadd_of_ne` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`zero_vadd` `Set.disjoint_vadd_set_right` `vadd_vadd` `neg_vadd_eq_iff`
`isBlock_iff_pairwiseDisjoint_range_vadd` 📖	mathematical	—	`IsBlock` `Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`Set.pairwiseDisjoint_range_iff`
`isBlock_iff_vadd_eq_of_mem` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`isBlock_iff_vadd_eq_of_nonempty` `Set.mem_inter_iff` `Set.mem_vadd_set` `exists_exists_and_eq_and`
`isBlock_iff_vadd_eq_of_nonempty` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`isBlock_iff_disjoint_vadd_of_ne` `Set.not_disjoint_iff_nonempty_inter` `not_imp_comm`
`isBlock_iff_vadd_eq_or_disjoint` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`isBlock_iff_disjoint_vadd_of_ne`
`isBlock_iff_vadd_eq_vadd_of_nonempty` 📖	mathematical	—	`IsBlock` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`Set.not_disjoint_iff_nonempty_inter` `not_imp_comm`
`isBlock_iff_vadd_eq_vadd_or_disjoint` 📖	mathematical	—	`IsBlock` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`isBlock_subtypeVal` 📖	mathematical	—	`IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `Set.image` `SubAddAction` `SetLike.instMembership` `SubAddAction.instSetLike` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `SubAddAction.inclusion.coe_eq` `image_vadd_set` `instAddActionSemiHomClassAddActionHom` `Set.image_eq_image` `SubAddAction.inclusion_injective` `Set.disjoint_image_iff`
`isBlock_top` 📖	mathematical	—	`IsBlock` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Top.top` `AddSubgroup.instTop` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `toAddSemigroupAction` `AddSubgroup.instAddAction`	—	`Equiv.forall_congr` `Equiv.forall_congr_left`
`isInvariantBlock_iff_isFixedBlock` 📖	mathematical	—	`IsInvariantBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `IsFixedBlock`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_vadd_set_iff` `IsFixedBlock.isInvariantBlock`
`stabilizer_orbit_eq` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `stabilizer`	`Set` `Set.addActionSet` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `orbit` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddSubgroup.toAddGroup` `toAddSemigroupAction` `AddSubgroup.instAddAction`	—	`AddSubgroup.ext` `mem_orbit_self` `add_mem_cancel_right` `AddSubgroup.instAddSubgroupClass` `mem_stabilizer_iff` `AddSemigroupAction.add_vadd` `AddSubmonoid.vadd_def` `vadd_orbit`
`vadd_orbit_eq_orbit_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction`	—	`Set.vadd_set_range` `Set.ext` `Set.mem_range` `AddSubgroup.Normal.conj_mem` `vadd_vadd` `neg_add_cancel_right` `AddSubgroup.Normal.conj_mem'` `vadd_neg_vadd`

AddAction.BlockMem

Definitions

Name	Category	Theorems
`instBoundedOrder` 📖	CompOp	3 math math: `coe_top`, `AddAction.isSimpleOrder_blockMem_iff_isPreprimitive`, `coe_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Bot.bot` `AddAction.BlockMem` `OrderBot.toBot` `Set.instLE` `BoundedOrder.toOrderBot` `instBoundedOrder` `Set.instSingletonSet`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Top.top` `AddAction.BlockMem` `OrderTop.toTop` `Set.instLE` `BoundedOrder.toOrderTop` `instBoundedOrder` `Set.univ`	—	—
`instNontrivial` 📖	mathematical	—	`Nontrivial` `AddAction.BlockMem`	—	`nontrivial_iff` `exists_ne` `Set.mem_singleton_iff` `Set.mem_univ`

AddAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroup` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction`	—	—
`disjoint_vadd_left` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vadd`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Disjoint.symm` `disjoint_vadd_right`
`disjoint_vadd_of_ne` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`AddAction.isBlock_iff_disjoint_vadd_of_ne`
`disjoint_vadd_right` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vadd`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`zero_vadd` `disjoint_vadd_set_vadd`
`disjoint_vadd_set_vadd` 📖	mathematical	`AddAction.IsBlock` `Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Set.vadd`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.iUnion_vadd_set` `Set.disjoint_iUnion₂_right` `Eq.trans_subset` `Set.vadd_set_subset_vadd`
`disjoint_vadd_vadd_set` 📖	mathematical	`AddAction.IsBlock` `Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `Set.vadd`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Disjoint.symm` `disjoint_vadd_set_vadd`
`empty` 📖	mathematical	—	`AddAction.IsBlock` `Set` `Set.instEmptyCollection`	—	`Set.vadd_set_empty` `disjoint_self`
`eq_univ_of_card_lt` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Nat.card` `Set.ncard`	`Set.univ`	—	`Set.eq_empty_or_nonempty` `Set.ncard_empty` `MulZeroClass.zero_mul` `not_lt_zero'` `ncard_block_add_ncard_orbit_eq` `Set.eq_of_subset_of_ncard_le` `Set.subset_univ` `Eq.ge` `Set.ncard_univ` `mul_one` `Set.toFinite` `Subtype.finite` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `mul_lt_mul_iff_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Set.ncard_pos` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `IsEmpty.exists_iff` `Finite.not_infinite` `Nat.card_eq_zero` `MulZeroClass.mul_zero`
`iInter` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Set.iInter`	—	`AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty` `Set.vadd_set_iInter` `Set.iInter_subset`
`image` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom` `AddAction.IsBlock`	`Set.image`	—	`Function.Surjective.forall` `image_vadd_setₛₗ` `instAddActionSemiHomClassAddActionHom` `Set.disjoint_image_of_injective`
`inter` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Set` `Set.instInter`	—	`AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty` `Set.vadd_set_inter`
`isBlockSystem` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.Nonempty`	`AddAction.IsBlockSystem` `Set.range` `Set` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`Set.mem_range` `Set.Nonempty.ne_empty` `Set.vadd_set_eq_empty` `AddAction.exists_vadd_eq` `Set.vadd_mem_vadd_set_iff` `vadd_eq_vadd_of_nonempty` `translate`
`ncard_block_add_ncard_orbit_eq` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.Nonempty`	`Set.ncard` `Set` `AddAction.orbit` `Set.vaddSet` `Nat.card`	—	`ncard_block_eq_relIndex` `AddAction.index_stabilizer` `AddSubgroup.relIndex_mul_index` `stabilizer_le` `AddAction.index_stabilizer_of_transitive`
`ncard_block_eq_relIndex` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership`	`Set.ncard` `AddSubgroup.relIndex` `AddAction.stabilizer` `Set.addActionSet`	—	`AddSubgroup.ext` `AddSubgroup.relIndex.eq_1` `AddAction.index_stabilizer` `orbit_stabilizer_eq`
`ncard_dvd_card` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.Nonempty`	`Set.ncard` `Nat.card`	—	`Dvd.intro` `ncard_block_add_ncard_orbit_eq`
`not_vadd_set_ssubset_vadd_set` 📖	mathematical	`AddAction.IsBlock`	`Set` `Set.instHasSSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `vadd_eq_vadd_of_subset` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset`
`of_addSubgroup_of_conjugate` 📖	mathematical	`AddAction.IsBlock` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction`	`AddSubgroup.map` `AddEquiv.toAddMonoidHom` `AddMonoid.toAddZeroClass` `DFunLike.coe` `Equiv` `Additive` `AddAut` `AddSemigroup.toAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `Additive.toMul` `AddMonoidHom` `AddZeroClass.toAddZero` `Additive.addZeroClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddAut.instGroup` `AddMonoidHom.instFunLike` `AddAut.conj` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`AddAction.isBlock_iff_vadd_eq_or_disjoint` `AddSubgroup.mem_map` `SetLike.coe_mem` `vadd_vadd` `neg_add_cancel_right` `vadd_eq_or_disjoint` `Set.disjoint_image_of_injective` `AddAction.injective`
`of_orbit` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddAction.stabilizer`	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddAction.orbit` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction`	—	`AddAction.isBlock_iff_vadd_eq_of_nonempty` `add_mem_cancel_left` `AddSubgroup.instAddSubgroupClass` `add_mem_cancel_right` `AddAction.mem_stabilizer_iff` `AddSemigroupAction.add_vadd` `neg_vadd_eq_iff` `AddSubmonoid.vadd_def` `AddAction.vadd_orbit`
`of_subset` 📖	mathematical	—	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.iInter` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`Set.eq_empty_or_nonempty` `Set.iInter_congr_Prop` `Set.vadd_set_empty` `Set.mem_empty_iff_false` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `univ` `Set.biInter_subset_of_mem` `AddAction.exists_vadd_eq` `Set.Finite.subset` `Set.Finite.map` `Set.mem_vadd_set_iff_neg_vadd_mem` `Set.mem_iInter` `vadd_vadd` `neg_add_rev` `AddAction.mem_stabilizer_iff` `AddAction.mem_stabilizer_set_iff_subset_vadd_set` `AddAction.isBlock_iff_vadd_eq_of_nonempty` `neg_vadd_vadd` `AddSemigroupAction.add_vadd` `neg_neg` `vadd_eq_iff_eq_neg_vadd`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`AddAction.IsBlock`	—	`Set.Subsingleton.induction_on` `empty` `singleton`
`orbit` 📖	mathematical	—	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddAction.orbit`	—	`AddAction.IsFixedBlock.isBlock` `AddAction.IsFixedBlock.orbit`
`orbit_of_normal` 📖	mathematical	—	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddAction.orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction`	—	`AddAction.isBlock_iff_vadd_eq_or_disjoint` `AddAction.vadd_orbit_eq_orbit_vadd` `AddAction.orbit.eq_or_disjoint`
`orbit_stabilizer_eq` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership`	`AddAction.orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `Set.addActionSet` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction`	—	`Set.ext` `Set.vadd_mem_vadd_set_iff` `AddAction.exists_vadd_eq` `vadd_eq_of_mem`
`pairwiseDisjoint_range_vadd` 📖	mathematical	`AddAction.IsBlock`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	`AddAction.isBlock_iff_pairwiseDisjoint_range_vadd`
`preimage` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`Set.preimage` `DFunLike.coe` `AddActionHom` `instFunLikeAddActionHom`	—	`AddGroup.preimage_vadd_setₛₗ` `instAddActionSemiHomClassAddActionHom` `Disjoint.preimage`
`singleton` 📖	mathematical	—	`AddAction.IsBlock` `Set` `Set.instSingletonSet`	—	`Set.vadd_set_singleton` `Set.singleton_eq_singleton_iff` `Set.disjoint_singleton_left` `Set.mem_singleton_iff`
`stabilizer_le` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership`	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddAction.stabilizer` `Set.addActionSet`	—	`vadd_eq_of_nonempty` `Set.vadd_mem_vadd_set_iff`
`subsingleton_of_card_lt` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Nat.card` `Set.ncard` `Set` `AddAction.orbit` `Set.vaddSet`	`Set.Subsingleton`	—	`Set.eq_empty_or_nonempty` `Set.ncard_empty` `Nat.instAtLeastTwoHAddOfNat` `Nat.ofNat_pos` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `not_le` `lt_iff_not_ge` `ncard_block_add_ncard_orbit_eq` `Set.ncard_le_one_iff_eq` `Set.toFinite` `Subtype.finite` `Set.subsingleton_empty` `Set.subsingleton_singleton`
`subtype_val_preimage` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`SubAddAction` `SetLike.instMembership` `SubAddAction.instSetLike` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left` `Set.preimage`	—	`preimage`
`translate` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`AddAction.isBlock_top` `AddSubgroup.map_comap_eq_self_of_surjective` `AddEquiv.surjective` `of_addSubgroup_of_conjugate` `AddSubgroup.comap_top`
`univ` 📖	mathematical	—	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.univ`	—	`AddAction.IsFixedBlock.isBlock` `AddAction.IsFixedBlock.univ`
`vadd_eq_of_mem` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd`	`Set.vaddSet`	—	`AddAction.isBlock_iff_vadd_eq_of_mem`
`vadd_eq_of_nonempty` 📖	—	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.Nonempty` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	—	`AddAction.isBlock_iff_vadd_eq_of_nonempty`
`vadd_eq_or_disjoint` 📖	mathematical	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`AddAction.isBlock_iff_vadd_eq_or_disjoint`
`vadd_eq_vadd_of_nonempty` 📖	—	`AddAction.IsBlock` `Set.Nonempty` `Set` `Set.instInter` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	—	`AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty`
`vadd_eq_vadd_of_subset` 📖	—	`AddAction.IsBlock` `Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet`	—	—	`Set.vadd_set_empty` `Set.vadd_set_eq_empty` `Disjoint.eq_bot_of_le`
`vadd_eq_vadd_or_disjoint` 📖	mathematical	`AddAction.IsBlock`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint`

AddAction.IsBlockSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_normal` 📖	mathematical	—	`AddAction.IsBlockSystem` `Set.range` `Set` `AddAction.orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction`	—	`AddAction.IsPartition.of_orbits` `AddAction.IsBlock.orbit_of_normal`

AddAction.IsFixedBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock` 📖	mathematical	`AddAction.IsFixedBlock`	`AddAction.IsBlock`	—	`disjoint_self` `IsEmpty.forall_iff` `instIsEmptyFalse`
`isInvariantBlock` 📖	mathematical	`AddAction.IsFixedBlock`	`AddAction.IsInvariantBlock`	—	`Eq.le`
`orbit` 📖	mathematical	—	`AddAction.IsFixedBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddAction.orbit`	—	`AddAction.vadd_orbit`
`univ` 📖	mathematical	—	`AddAction.IsFixedBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.univ`	—	`Set.vadd_set_univ`

AddAction.IsInvariantBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock` 📖	mathematical	`AddAction.IsInvariantBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`AddAction.IsBlock`	—	`AddAction.IsFixedBlock.isBlock` `isFixedBlock`
`isFixedBlock` 📖	mathematical	`AddAction.IsInvariantBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`AddAction.IsFixedBlock`	—	`AddAction.isInvariantBlock_iff_isFixedBlock`

AddAction.IsPartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_orbits` 📖	mathematical	—	`Setoid.IsPartition` `Set.range` `Set` `AddAction.orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty` `AddAction.orbit.pairwiseDisjoint` `AddAction.mem_orbit_self` `Set.Nonempty.ne_empty` `AddAction.nonempty_orbit`

AddAction.IsTrivialBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom` `AddAction.IsTrivialBlock`	`Set.image`	—	`Set.Subsingleton.image` `Set.image_univ` `Set.range_eq_univ`
`isBlock` 📖	mathematical	`AddAction.IsTrivialBlock`	`AddAction.IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`AddAction.IsBlock.of_subsingleton` `AddAction.IsBlock.univ`
`preimage` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom` `AddAction.IsTrivialBlock`	`Set.preimage`	—	`Set.Subsingleton.preimage` `Set.preimage_univ`
`vadd` 📖	mathematical	`AddAction.IsTrivialBlock`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Function.Injective.subsingleton_image_iff` `AddAction.injective` `Set.image_vadd` `Set.image_univ_of_surjective` `AddAction.surjective`
`vadd_iff` 📖	mathematical	—	`AddAction.IsTrivialBlock` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`neg_vadd_vadd` `vadd`

AddAction.orbit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_disjoint` 📖	mathematical	—	`AddAction.orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.not_disjoint_iff` `AddAction.orbit_eq_iff` `em`
`pairwiseDisjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `AddAction.orbit` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `eq_or_disjoint`

MulAction

Definitions

Name	Category	Theorems
`BlockMem` 📖	CompOp	4 math math: `BlockMem.coe_top`, `BlockMem.instNontrivial`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `BlockMem.coe_bot`
`IsBlock` 📖	MathDef	25 math math: `IsBlock.of_subset`, `isBlock_iff_smul_eq_of_mem`, `BlockMem.coe_top`, `isBlock_iff_smul_eq_or_disjoint`, `isBlock_top`, `IsBlock.orbit_of_normal`, `isBlock_subgroup'`, `IsTrivialBlock.isBlock`, `isBlock_iff_smul_eq_smul_of_nonempty`, `IsBlock.univ`, `IsBlock.empty`, `IsInvariantBlock.isBlock`, `IsBlock.of_subsingleton`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `BlockMem.coe_bot`, `isBlock_subgroup`, `isBlock_iff_smul_eq_smul_or_disjoint`, `isBlock_iff_disjoint_smul_of_ne`, `IsBlock.orbit`, `isBlock_iff_pairwiseDisjoint_range_smul`, `isBlock_iff_smul_eq_of_nonempty`, `IsFixedBlock.isBlock`, `IsBlock.of_orbit`, `IsBlock.singleton`, `isBlock_subtypeVal`
`IsBlockSystem` 📖	MathDef	2 math math: `IsBlock.isBlockSystem`, `IsBlockSystem.of_normal`
`IsFixedBlock` 📖	MathDef	4 math math: `isInvariantBlock_iff_isFixedBlock`, `IsFixedBlock.orbit`, `IsFixedBlock.univ`, `IsInvariantBlock.isFixedBlock`
`IsInvariantBlock` 📖	MathDef	2 math math: `isInvariantBlock_iff_isFixedBlock`, `IsFixedBlock.isInvariantBlock`
`IsTrivialBlock` 📖	MathDef	5 math math: `isTrivialBlock_of_card_le_two`, `AlternatingGroup.isTrivialBlock_of_isBlock`, `alternatingGroup.isTrivialBlock_of_isBlock`, `IsPreprimitive.isTrivialBlock_of_isBlock`, `IsTrivialBlock.smul_iff`
`block_stabilizerOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock_iff_disjoint_smul_of_ne` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.smulSet`	—	`one_smul` `smul_smul`
`isBlock_iff_pairwiseDisjoint_range_smul` 📖	mathematical	—	`IsBlock` `Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `Set.smulSet`	—	`Set.pairwiseDisjoint_range_iff`
`isBlock_iff_smul_eq_of_mem` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set` `Set.smulSet`	—	—
`isBlock_iff_smul_eq_of_nonempty` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set` `Set.smulSet`	—	—
`isBlock_iff_smul_eq_or_disjoint` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set` `Set.smulSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`isBlock_iff_disjoint_smul_of_ne`
`isBlock_iff_smul_eq_smul_of_nonempty` 📖	mathematical	—	`IsBlock` `Set` `Set.smulSet`	—	—
`isBlock_iff_smul_eq_smul_or_disjoint` 📖	mathematical	—	`IsBlock` `Set` `Set.smulSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`isBlock_subgroup` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `SetLike.coe`	—	`smul_coe_set` `smul_assoc` `Set.isScalarTower`
`isBlock_subgroup'` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `SetLike.coe`	—	`op_smul_coe_set` `smul_assoc` `Set.isScalarTower` `MulOpposite.op_smul`
`isBlock_subtypeVal` 📖	mathematical	—	`IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set.image` `SubMulAction` `SetLike.instMembership` `SubMulAction.instSetLike` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `SubMulAction.inclusion.coe_eq` `image_smul_set` `instMulActionSemiHomClassMulActionHom` `Set.image_eq_image` `SubMulAction.inclusion_injective` `Set.disjoint_image_iff`
`isBlock_top` 📖	mathematical	—	`IsBlock` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Top.top` `Subgroup.instTop` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `toSemigroupAction` `Subgroup.instMulAction`	—	`Equiv.forall_congr` `Equiv.forall_congr_left`
`isInvariantBlock_iff_isFixedBlock` 📖	mathematical	—	`IsInvariantBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `IsFixedBlock`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_smul_set_iff` `IsFixedBlock.isInvariantBlock`
`smul_orbit_eq_orbit_smul` 📖	mathematical	—	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.instMulAction`	—	`Set.smul_set_range` `Set.ext` `Subgroup.Normal.conj_mem` `smul_smul` `inv_mul_cancel_right` `Subgroup.Normal.conj_mem'` `smul_inv_smul`
`stabilizer_orbit_eq` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `stabilizer`	`Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `orbit` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Subgroup.toGroup` `toSemigroupAction` `Subgroup.instMulAction`	—	`Subgroup.ext` `mem_orbit_self` `mul_mem_cancel_right` `Subgroup.instSubgroupClass` `Submonoid.smul_def` `mem_stabilizer_iff` `smul_orbit`

MulAction.BlockMem

Definitions

Name	Category	Theorems
`instBoundedOrder` 📖	CompOp	3 math math: `coe_top`, `MulAction.isSimpleOrder_blockMem_iff_isPreprimitive`, `coe_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`Set` `Set.instMembership` `MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Bot.bot` `MulAction.BlockMem` `OrderBot.toBot` `Set.instLE` `BoundedOrder.toOrderBot` `instBoundedOrder` `Set.instSingletonSet`	—	—
`coe_top` 📖	mathematical	—	`Set` `Set.instMembership` `MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Top.top` `MulAction.BlockMem` `OrderTop.toTop` `Set.instLE` `BoundedOrder.toOrderTop` `instBoundedOrder` `Set.univ`	—	—
`instNontrivial` 📖	mathematical	—	`Nontrivial` `MulAction.BlockMem`	—	`nontrivial_iff` `exists_ne` `Set.mem_singleton_iff` `Set.mem_univ`

MulAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_smul_left` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Set` `Set.instHasSubset` `Set.smul`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Disjoint.symm` `disjoint_smul_right`
`disjoint_smul_of_ne` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.smulSet`	—	`MulAction.isBlock_iff_disjoint_smul_of_ne`
`disjoint_smul_right` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Set` `Set.instHasSubset` `Set.smul`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`one_smul` `disjoint_smul_set_smul`
`disjoint_smul_set_smul` 📖	mathematical	`MulAction.IsBlock` `Set` `Set.instHasSubset` `Set.smulSet` `Set.smul`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.iUnion_smul_set` `Set.disjoint_iUnion₂_right` `Eq.trans_subset` `Set.smul_set_subset_smul`
`disjoint_smul_smul_set` 📖	mathematical	`MulAction.IsBlock` `Set` `Set.instHasSubset` `Set.smulSet` `Set.smul`	`Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Disjoint.symm` `disjoint_smul_set_smul`
`empty` 📖	mathematical	—	`MulAction.IsBlock` `Set` `Set.instEmptyCollection`	—	`Set.smul_set_empty`
`eq_univ_of_card_lt` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Nat.card` `Set.ncard`	`Set.univ`	—	`Set.eq_empty_or_nonempty` `Set.ncard_empty` `MulZeroClass.zero_mul` `ncard_block_mul_ncard_orbit_eq` `Set.eq_of_subset_of_ncard_le` `Set.subset_univ` `Eq.ge` `Set.ncard_univ` `mul_one` `Set.toFinite` `Subtype.finite` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_lt_right` `mul_lt_mul_iff_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Set.ncard_pos` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `IsEmpty.exists_iff` `Finite.not_infinite` `Nat.card_eq_zero` `MulZeroClass.mul_zero`
`iInter` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Set.iInter`	—	`Set.smul_set_iInter` `Set.iInter_subset`
`image` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom` `MulAction.IsBlock`	`Set.image`	—	`Function.Surjective.forall` `instMulActionSemiHomClassMulActionHom` `Set.disjoint_image_of_injective`
`inter` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Set` `Set.instInter`	—	`Set.smul_set_inter`
`isBlockSystem` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.Nonempty`	`MulAction.IsBlockSystem` `Set.range` `Set` `Set.smulSet`	—	`Set.Nonempty.ne_empty` `MulAction.exists_smul_eq` `smul_eq_smul_of_nonempty` `translate`
`ncard_block_eq_relIndex` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership`	`Set.ncard` `Subgroup.relIndex` `MulAction.stabilizer` `Set.mulActionSet`	—	`Subgroup.ext` `Subgroup.relIndex.eq_1` `MulAction.index_stabilizer` `orbit_stabilizer_eq`
`ncard_block_mul_ncard_orbit_eq` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.Nonempty`	`Set.ncard` `Set` `MulAction.orbit` `Set.smulSet` `Nat.card`	—	`ncard_block_eq_relIndex` `MulAction.index_stabilizer` `Subgroup.relIndex_mul_index` `stabilizer_le` `MulAction.index_stabilizer_of_transitive`
`ncard_dvd_card` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.Nonempty`	`Set.ncard` `Nat.card`	—	`Dvd.intro` `ncard_block_mul_ncard_orbit_eq`
`not_smul_set_ssubset_smul_set` 📖	mathematical	`MulAction.IsBlock`	`Set` `Set.instHasSSubset` `Set.smulSet`	—	`HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `smul_eq_smul_of_subset` `HasSSubset.SSubset.subset` `Set.instIsNonstrictStrictOrderSubsetSSubset`
`of_orbit` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer`	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.orbit` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.instMulAction`	—	`MulAction.isBlock_iff_smul_eq_of_nonempty` `mul_mem_cancel_left` `Subgroup.instSubgroupClass` `mul_mem_cancel_right` `SemigroupAction.mul_smul` `Submonoid.smul_def` `MulAction.smul_orbit`
`of_subgroup_of_conjugate` 📖	mathematical	`MulAction.IsBlock` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction`	`Subgroup.map` `MulEquiv.toMonoidHom` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `MulAut.instGroup` `MonoidHom.instFunLike` `MulAut.conj` `Set` `Set.smulSet`	—	`MulAction.isBlock_iff_smul_eq_or_disjoint` `Subgroup.mem_map` `SetLike.coe_mem` `smul_smul` `inv_mul_cancel_right` `smul_eq_or_disjoint` `Set.disjoint_image_of_injective` `MulAction.injective`
`of_subset` 📖	mathematical	—	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.iInter` `Set` `Set.instMembership` `Set.smulSet`	—	`Set.eq_empty_or_nonempty` `Set.iInter_congr_Prop` `Set.smul_set_empty` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `Set.biInter_subset_of_mem` `MulAction.exists_smul_eq` `Set.Finite.subset` `Set.Finite.map` `smul_smul` `MulAction.mem_stabilizer_iff` `MulAction.mem_stabilizer_set_iff_subset_smul_set` `MulAction.isBlock_iff_smul_eq_of_nonempty` `inv_smul_smul` `SemigroupAction.mul_smul` `Set.mem_smul_set_iff_inv_smul_mem` `inv_inv` `smul_eq_iff_eq_inv_smul`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton`	`MulAction.IsBlock`	—	`Set.Subsingleton.induction_on` `empty` `singleton`
`orbit` 📖	mathematical	—	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.orbit`	—	`MulAction.IsFixedBlock.isBlock` `MulAction.IsFixedBlock.orbit`
`orbit_of_normal` 📖	mathematical	—	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.instMulAction`	—	`MulAction.isBlock_iff_smul_eq_or_disjoint` `MulAction.smul_orbit_eq_orbit_smul` `MulAction.orbit.eq_or_disjoint`
`orbit_stabilizer_eq` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership`	`MulAction.orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Set.mulActionSet` `Subgroup.toGroup` `Subgroup.instMulAction`	—	`Set.ext` `Set.smul_mem_smul_set_iff` `MulAction.exists_smul_eq` `smul_eq_of_mem`
`pairwiseDisjoint_range_smul` 📖	mathematical	`MulAction.IsBlock`	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `Set.smulSet`	—	`MulAction.isBlock_iff_pairwiseDisjoint_range_smul`
`preimage` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Set.preimage` `DFunLike.coe` `MulActionHom` `instFunLikeMulActionHom`	—	`Group.preimage_smul_setₛₗ` `instMulActionSemiHomClassMulActionHom` `Disjoint.preimage`
`singleton` 📖	mathematical	—	`MulAction.IsBlock` `Set` `Set.instSingletonSet`	—	`Set.smul_set_singleton`
`smul_eq_of_mem` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership`	`Set.smulSet`	—	`MulAction.isBlock_iff_smul_eq_of_mem`
`smul_eq_of_nonempty` 📖	—	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.Nonempty` `Set` `Set.instInter` `Set.smulSet`	—	—	`MulAction.isBlock_iff_smul_eq_of_nonempty`
`smul_eq_or_disjoint` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Set` `Set.smulSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`MulAction.isBlock_iff_smul_eq_or_disjoint`
`smul_eq_smul_of_nonempty` 📖	—	`MulAction.IsBlock` `Set.Nonempty` `Set` `Set.instInter` `Set.smulSet`	—	—	`MulAction.isBlock_iff_smul_eq_smul_of_nonempty`
`smul_eq_smul_of_subset` 📖	—	`MulAction.IsBlock` `Set` `Set.instHasSubset` `Set.smulSet`	—	—	`Set.smul_set_empty` `Disjoint.eq_bot_of_le`
`smul_eq_smul_or_disjoint` 📖	mathematical	`MulAction.IsBlock`	`Set` `Set.smulSet` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`MulAction.isBlock_iff_smul_eq_smul_or_disjoint`
`stabilizer_le` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set` `Set.instMembership`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MulAction.stabilizer` `Set.mulActionSet`	—	`smul_eq_of_nonempty` `Set.smul_mem_smul_set_iff`
`subgroup` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Subgroup.instMulAction`	—	—
`subsingleton_of_card_lt` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Nat.card` `Set.ncard` `Set` `MulAction.orbit` `Set.smulSet`	`Set.Subsingleton`	—	`Set.eq_empty_or_nonempty` `Set.ncard_empty` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `not_le` `lt_iff_not_ge` `ncard_block_mul_ncard_orbit_eq` `Set.ncard_le_one_iff_eq` `Set.toFinite` `Subtype.finite` `Set.subsingleton_empty` `Set.subsingleton_singleton`
`subtype_val_preimage` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`SubMulAction` `SetLike.instMembership` `SubMulAction.instSetLike` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left` `Set.preimage`	—	`preimage`
`translate` 📖	mathematical	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`Set` `Set.smulSet`	—	`MulAction.isBlock_top` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Subgroup.map_comap_eq_self_of_surjective` `MulEquiv.surjective` `of_subgroup_of_conjugate` `Subgroup.comap_top`
`univ` 📖	mathematical	—	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.univ`	—	`MulAction.IsFixedBlock.isBlock` `MulAction.IsFixedBlock.univ`

MulAction.IsBlockSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_normal` 📖	mathematical	—	`MulAction.IsBlockSystem` `Set.range` `Set` `MulAction.orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction`	—	`MulAction.IsPartition.of_orbits` `MulAction.IsBlock.orbit_of_normal`

MulAction.IsFixedBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock` 📖	mathematical	`MulAction.IsFixedBlock`	`MulAction.IsBlock`	—	`instIsEmptyFalse`
`isInvariantBlock` 📖	mathematical	`MulAction.IsFixedBlock`	`MulAction.IsInvariantBlock`	—	`Eq.le`
`orbit` 📖	mathematical	—	`MulAction.IsFixedBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.orbit`	—	`MulAction.smul_orbit`
`univ` 📖	mathematical	—	`MulAction.IsFixedBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.univ`	—	`Set.smul_set_univ`

MulAction.IsInvariantBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBlock` 📖	mathematical	`MulAction.IsInvariantBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MulAction.IsBlock`	—	`MulAction.IsFixedBlock.isBlock` `isFixedBlock`
`isFixedBlock` 📖	mathematical	`MulAction.IsInvariantBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MulAction.IsFixedBlock`	—	`MulAction.isInvariantBlock_iff_isFixedBlock`

MulAction.IsPartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_orbits` 📖	mathematical	—	`Setoid.IsPartition` `Set.range` `Set` `MulAction.orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty` `MulAction.orbit.pairwiseDisjoint` `MulAction.mem_orbit_self` `Set.Nonempty.ne_empty` `MulAction.nonempty_orbit`

MulAction.IsTrivialBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instFunLikeMulActionHom` `MulAction.IsTrivialBlock`	`Set.image`	—	`Set.Subsingleton.image` `Set.image_univ`
`isBlock` 📖	mathematical	`MulAction.IsTrivialBlock`	`MulAction.IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`MulAction.IsBlock.of_subsingleton` `MulAction.IsBlock.univ`
`preimage` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instFunLikeMulActionHom` `MulAction.IsTrivialBlock`	`Set.preimage`	—	`Set.Subsingleton.preimage` `Set.preimage_univ`
`smul` 📖	mathematical	`MulAction.IsTrivialBlock`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Function.Injective.subsingleton_image_iff` `MulAction.injective` `Set.image_smul` `Set.image_univ_of_surjective` `MulAction.surjective`
`smul_iff` 📖	mathematical	—	`MulAction.IsTrivialBlock` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`inv_smul_smul` `smul`

MulAction.orbit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_disjoint` 📖	mathematical	—	`MulAction.orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`em`
`pairwiseDisjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `MulAction.orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `eq_or_disjoint`

---

← Back to Index