MulOpposite

📁 Source: Mathlib/Algebra/Group/Subgroup/MulOpposite.lean

Statistics

Metric	Count
Definitions `equivOp`, `op`, `opEquiv`, `unop`, `equivOp`, `op`, `opEquiv`, `unop`	8
Theorems `coe_op`, `coe_unop`, `equivOp_apply_coe`, `equivOp_symm_apply_coe`, `le_op_iff`, `mem_op`, `mem_unop`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_inj`, `op_injective`, `op_le_iff`, `op_le_op_iff`, `op_normalizer`, `op_toAddSubmonoid`, `op_toSubsemigroup`, `op_unop`, `unop_inj`, `unop_injective`, `unop_le_unop_iff`, `unop_normalizer`, `unop_op`, `unop_toAddSubmonoid`, `unop_toSubsemigroup`, `coe_op`, `coe_unop`, `equivOp_apply_coe`, `equivOp_symm_apply_coe`, `le_op_iff`, `mem_op`, `mem_unop`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_inj`, `op_injective`, `op_le_iff`, `op_le_op_iff`, `op_normalizer`, `op_toSubmonoid`, `op_toSubsemigroup`, `op_unop`, `unop_inj`, `unop_injective`, `unop_le_unop_iff`, `unop_normalizer`, `unop_op`, `unop_toSubmonoid`, `unop_toSubsemigroup`	48
Total	56

AddSubgroup

Definitions

Name	Category	Theorems
`equivOp` 📖	CompOp	2 math math: `equivOp_apply_coe`, `equivOp_symm_apply_coe`
`op` 📖	CompOp	47 math math: `normal_op`, `op_inf`, `Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp`, `unop_sInf`, `op_le_iff`, `op_sInf`, `op_normalizer`, `AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `AddAction.stabilizer_op_addSubgroup`, `op.instNormal`, `le_op_iff`, `op_top`, `op_toAddSubmonoid`, `op_le_op_iff`, `op_bot`, `op_toSubsemigroup`, `vadd_opposite_add`, `op_sup`, `op_inj`, `op_closure`, `QuotientAddGroup.sound`, `coe_op`, `mem_op`, `isAddQuotientCoveringMap`, `op_unop`, `op_sSup`, `Normal.op`, `op_iInf`, `opEquiv_apply`, `properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite`, `op_injective`, `AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume`, `QuotientAddGroup.orbit_eq_out_vadd`, `AddAction.right_quotientAction`, `op_iSup`, `AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `equivOp_apply_coe`, `op_eq_bot`, `unop_sSup`, `vadd_opposite_image_add_preimage`, `instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe`, `unop_op`, `isAddFundamentalDomain_Ioc'`, `op_eq_top`, `QuotientAddGroup.orbit_mk_eq_vadd`, `instCountableSubtypeAddOppositeMemOp`, `equivOp_symm_apply_coe`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `opEquiv_apply`
`unop` 📖	CompOp	30 math math: `AddAction.stabilizer_addSubgroup_op`, `coe_unop`, `unop_normalizer`, `unop_sInf`, `op_le_iff`, `unop_closure`, `op_sInf`, `unop_inf`, `le_op_iff`, `unop_iSup`, `unop_injective`, `unop_toSubsemigroup`, `unop.instNormal`, `unop_sup`, `opEquiv_symm_apply`, `op_unop`, `op_sSup`, `unop_eq_top`, `unop_eq_bot`, `unop_bot`, `unop_iInf`, `unop_inj`, `Normal.unop`, `unop_toAddSubmonoid`, `unop_top`, `mem_unop`, `unop_sSup`, `normal_unop`, `unop_op`, `unop_le_unop_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_op` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instSetLike` `op` `Set.preimage` `AddOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `instSetLike` `unop` `Set.preimage` `AddOpposite` `AddOpposite.op` `AddOpposite.instAddGroup`	—	—
`equivOp_apply_coe` 📖	mathematical	—	`AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `instSetLike` `op` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOp` `AddOpposite.op`	—	—
`equivOp_symm_apply_coe` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `AddOpposite` `AddOpposite.instAddGroup` `op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOp` `AddOpposite.unop`	—	—
`le_op_iff` 📖	mathematical	—	`AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`mem_op` 📖	mathematical	—	`AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `instSetLike` `op` `AddOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `unop` `AddOpposite` `AddOpposite.instAddGroup` `AddOpposite.op`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_inj` 📖	mathematical	—	`op`	—	`RelIso.eq_iff_eq`
`op_injective` 📖	mathematical	—	`AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `op`	—	`OrderIso.injective`
`op_le_iff` 📖	mathematical	—	`AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `AddOpposite.op_surjective`
`op_normalizer` 📖	mathematical	—	`op` `normalizer` `AddOpposite` `AddOpposite.instAddGroup`	—	`ext` `mem_op` `mem_normalizer_iff'` `AddOpposite.forall`
`op_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `AddOpposite` `AddOpposite.instAddGroup` `op` `AddSubmonoid.op` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`op_toSubsemigroup` 📖	mathematical	—	`AddSubmonoid.toAddSubsemigroup` `AddOpposite` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddOpposite.instAddGroup` `toAddSubmonoid` `op` `AddSubsemigroup.op` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_inj` 📖	mathematical	—	`unop`	—	`RelIso.eq_iff_eq`
`unop_injective` 📖	mathematical	—	`AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `unop`	—	`OrderIso.injective`
`unop_le_unop_iff` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `AddOpposite` `AddOpposite.instAddGroup`	—	`Function.Surjective.forall` `AddOpposite.unop_surjective`
`unop_normalizer` 📖	mathematical	—	`unop` `normalizer` `AddOpposite` `AddOpposite.instAddGroup`	—	`op_unop` `op_normalizer`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `unop` `AddSubmonoid.unop` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddOpposite` `AddOpposite.instAddGroup`	—	—
`unop_toSubsemigroup` 📖	mathematical	—	`AddSubmonoid.toAddSubsemigroup` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSubmonoid` `unop` `AddSubsemigroup.unop` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddOpposite` `AddOpposite.instAddGroup`	—	—

Subgroup

Definitions

Name	Category	Theorems
`equivOp` 📖	CompOp	2 math math: `equivOp_symm_apply_coe`, `equivOp_apply_coe`
`op` 📖	CompOp	43 math math: `instCountableSubtypeMulOppositeMemOp`, `equivOp_symm_apply_coe`, `op_le_op_iff`, `op_iSup`, `op_bot`, `op_iInf`, `MulAction.right_quotientAction`, `mem_op`, `op_top`, `op_inf`, `smul_opposite_image_mul_preimage`, `normal_op`, `op_normalizer`, `op_toSubsemigroup`, `Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp`, `properlyDiscontinuousSMul_opposite_of_tendsto_cofinite`, `Normal.op`, `unop_sInf`, `MulAction.stabilizer_op_subgroup`, `QuotientGroup.orbit_eq_out_smul`, `op_eq_top`, `op_sInf`, `equivOp_apply_coe`, `smul_opposite_mul`, `instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe`, `op_closure`, `op_unop`, `op_injective`, `op_sup`, `unop_sSup`, `QuotientGroup.orbit_mk_eq_smul`, `op_toSubmonoid`, `coe_op`, `unop_op`, `op_eq_bot`, `le_op_iff`, `op.instNormal`, `op_sSup`, `op_le_iff`, `QuotientGroup.sound`, `op_inj`, `isQuotientCoveringMap`, `opEquiv_apply`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `opEquiv_apply`
`unop` 📖	CompOp	30 math math: `unop_inf`, `unop_closure`, `unop_eq_bot`, `unop_normalizer`, `MulAction.stabilizer_subgroup_op`, `unop_sInf`, `unop_inj`, `op_sInf`, `unop_toSubsemigroup`, `coe_unop`, `opEquiv_symm_apply`, `unop_eq_top`, `unop_iSup`, `unop_injective`, `unop.instNormal`, `op_unop`, `unop_sSup`, `unop_bot`, `unop_op`, `le_op_iff`, `unop_le_unop_iff`, `Normal.unop`, `op_sSup`, `mem_unop`, `unop_sup`, `op_le_iff`, `normal_unop`, `unop_toSubmonoid`, `unop_iInf`, `unop_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_op` 📖	mathematical	—	`SetLike.coe` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instSetLike` `op` `Set.preimage` `MulOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `Subgroup` `instSetLike` `unop` `Set.preimage` `MulOpposite` `MulOpposite.op` `MulOpposite.instGroup`	—	—
`equivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `instSetLike` `op` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivOp` `MulOpposite.op`	—	—
`equivOp_symm_apply_coe` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `Equiv` `MulOpposite` `MulOpposite.instGroup` `op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivOp` `MulOpposite.unop`	—	—
`le_op_iff` 📖	mathematical	—	`Subgroup` `MulOpposite` `MulOpposite.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`mem_op` 📖	mathematical	—	`MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `instSetLike` `op` `MulOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `unop` `MulOpposite` `MulOpposite.instGroup` `MulOpposite.op`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_inj` 📖	mathematical	—	`op`	—	`RelIso.eq_iff_eq`
`op_injective` 📖	mathematical	—	`Subgroup` `MulOpposite` `MulOpposite.instGroup` `op`	—	`OrderIso.injective`
`op_le_iff` 📖	mathematical	—	`Subgroup` `MulOpposite` `MulOpposite.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`Subgroup` `MulOpposite` `MulOpposite.instGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_normalizer` 📖	mathematical	—	`op` `normalizer` `MulOpposite` `MulOpposite.instGroup`	—	`ext`
`op_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `MulOpposite` `MulOpposite.instGroup` `op` `Submonoid.op` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`op_toSubsemigroup` 📖	mathematical	—	`Submonoid.toSubsemigroup` `MulOpposite` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOpposite.instGroup` `toSubmonoid` `op` `Subsemigroup.op` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_inj` 📖	mathematical	—	`unop`	—	`RelIso.eq_iff_eq`
`unop_injective` 📖	mathematical	—	`Subgroup` `MulOpposite` `MulOpposite.instGroup` `unop`	—	`OrderIso.injective`
`unop_le_unop_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `MulOpposite` `MulOpposite.instGroup`	—	`Function.Surjective.forall` `MulOpposite.unop_surjective`
`unop_normalizer` 📖	mathematical	—	`unop` `normalizer` `MulOpposite` `MulOpposite.instGroup`	—	`op_unop` `op_normalizer`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `unop` `Submonoid.unop` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOpposite` `MulOpposite.instGroup`	—	—
`unop_toSubsemigroup` 📖	mathematical	—	`Submonoid.toSubsemigroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSubmonoid` `unop` `Subsemigroup.unop` `Semigroup.toMul` `Monoid.toSemigroup` `MulOpposite` `MulOpposite.instGroup`	—	—

---

← Back to Index