MulOppositeLemmas

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

Statistics

Metric	Count
Definitions `instEncodableSubtypeAddOppositeMemOp`, `instVAdd`, `instEncodableSubtypeMulOppositeMemOp`, `instSMul`	4
Theorems `of_op`, `of_unop`, `op`, `unop`, `instCountableSubtypeAddOppositeMemOp`, `normal_op`, `normal_unop`, `instNormal`, `op_bot`, `op_closure`, `op_eq_bot`, `op_eq_top`, `op_iInf`, `op_iSup`, `op_inf`, `op_sInf`, `op_sSup`, `op_sup`, `op_top`, `instNormal`, `unop_bot`, `unop_closure`, `unop_eq_bot`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_top`, `vadd_opposite_add`, `of_op`, `of_unop`, `op`, `unop`, `instCountableSubtypeMulOppositeMemOp`, `normal_op`, `normal_unop`, `instNormal`, `op_bot`, `op_closure`, `op_eq_bot`, `op_eq_top`, `op_iInf`, `op_iSup`, `op_inf`, `op_sInf`, `op_sSup`, `op_sup`, `op_top`, `smul_opposite_mul`, `instNormal`, `unop_bot`, `unop_closure`, `unop_eq_bot`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_top`	64
Total	68

AddSubgroup

Definitions

Name	Category	Theorems
`instEncodableSubtypeAddOppositeMemOp` 📖	CompOp	—
`instVAdd` 📖	CompOp	7 math math: `AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `vadd_opposite_add`, `QuotientAddGroup.sound`, `properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite`, `AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `vadd_opposite_image_add_preimage`, `isAddFundamentalDomain_Ioc'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCountableSubtypeAddOppositeMemOp` 📖	mathematical	—	`Countable` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `instSetLike` `op`	—	`Countable.of_equiv`
`normal_op` 📖	mathematical	—	`Normal` `AddOpposite` `AddOpposite.instAddGroup` `op`	—	`normalizer_eq_top_iff` `op_normalizer` `op_eq_top`
`normal_unop` 📖	mathematical	—	`Normal` `unop` `AddOpposite` `AddOpposite.instAddGroup`	—	`normal_op` `op_unop`
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `AddSubgroup` `instBot` `AddOpposite` `AddOpposite.instAddGroup`	—	`OrderIso.map_bot`
`op_closure` 📖	mathematical	—	`op` `closure` `AddOpposite` `AddOpposite.instAddGroup` `Set.preimage` `AddOpposite.unop`	—	`op_sInf` `Function.Surjective.forall` `AddOpposite.unop_surjective`
`op_eq_bot` 📖	mathematical	—	`op` `Bot.bot` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instBot`	—	`op_injective` `op_bot`
`op_eq_top` 📖	mathematical	—	`op` `Top.top` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instTop`	—	`op_injective` `op_top`
`op_iInf` 📖	mathematical	—	`op` `iInf` `AddSubgroup` `instInfSet` `AddOpposite` `AddOpposite.instAddGroup`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `AddSubgroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddGroup`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `AddSubgroup` `instMin` `AddOpposite` `AddOpposite.instAddGroup`	—	—
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `AddSubgroup` `instInfSet` `AddOpposite` `AddOpposite.instAddGroup` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `AddSubgroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddGroup` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `AddOpposite` `AddOpposite.instAddGroup`	—	`OrderIso.map_sup`
`op_top` 📖	mathematical	—	`op` `Top.top` `AddSubgroup` `instTop` `AddOpposite` `AddOpposite.instAddGroup`	—	—
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instBot`	—	`OrderIso.map_bot`
`unop_closure` 📖	mathematical	—	`unop` `closure` `AddOpposite` `AddOpposite.instAddGroup` `Set.preimage` `AddOpposite.op`	—	`op_unop` `op_closure` `Set.preimage_preimage`
`unop_eq_bot` 📖	mathematical	—	`unop` `Bot.bot` `AddSubgroup` `instBot` `AddOpposite` `AddOpposite.instAddGroup`	—	`unop_injective` `unop_bot`
`unop_eq_top` 📖	mathematical	—	`unop` `Top.top` `AddSubgroup` `instTop` `AddOpposite` `AddOpposite.instAddGroup`	—	`unop_injective` `unop_top`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instInfSet`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instMin`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instInfSet` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`OrderIso.map_sup`
`unop_top` 📖	mathematical	—	`unop` `Top.top` `AddSubgroup` `AddOpposite` `AddOpposite.instAddGroup` `instTop`	—	—
`vadd_opposite_add` 📖	mathematical	—	`HVAdd.hVAdd` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `SetLike.instMembership` `instSetLike` `op` `instHVAdd` `instVAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add_assoc`

AddSubgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_op` 📖	mathematical	—	`AddSubgroup.Normal`	—	`AddSubgroup.normal_op`
`of_unop` 📖	mathematical	—	`AddSubgroup.Normal` `AddOpposite` `AddOpposite.instAddGroup`	—	`AddSubgroup.normal_unop`
`op` 📖	mathematical	—	`AddSubgroup.Normal` `AddOpposite` `AddOpposite.instAddGroup` `AddSubgroup.op`	—	`AddSubgroup.normal_op`
`unop` 📖	mathematical	—	`AddSubgroup.Normal` `AddSubgroup.unop`	—	`AddSubgroup.normal_unop`

AddSubgroup.op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormal` 📖	mathematical	—	`AddSubgroup.Normal` `AddOpposite` `AddOpposite.instAddGroup` `AddSubgroup.op`	—	`AddSubgroup.Normal.op`

AddSubgroup.unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormal` 📖	mathematical	—	`AddSubgroup.Normal` `AddSubgroup.unop`	—	`AddSubgroup.Normal.unop`

Subgroup

Definitions

Name	Category	Theorems
`instEncodableSubtypeMulOppositeMemOp` 📖	CompOp	—
`instSMul` 📖	CompOp	4 math math: `smul_opposite_image_mul_preimage`, `properlyDiscontinuousSMul_opposite_of_tendsto_cofinite`, `smul_opposite_mul`, `QuotientGroup.sound`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCountableSubtypeMulOppositeMemOp` 📖	mathematical	—	`Countable` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `instSetLike` `op`	—	`Countable.of_equiv`
`normal_op` 📖	mathematical	—	`Normal` `MulOpposite` `MulOpposite.instGroup` `op`	—	—
`normal_unop` 📖	mathematical	—	`Normal` `unop` `MulOpposite` `MulOpposite.instGroup`	—	`normal_op` `op_unop`
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `Subgroup` `instBot` `MulOpposite` `MulOpposite.instGroup`	—	`OrderIso.map_bot`
`op_closure` 📖	mathematical	—	`op` `closure` `MulOpposite` `MulOpposite.instGroup` `Set.preimage` `MulOpposite.unop`	—	`op_sInf` `Function.Surjective.forall` `MulOpposite.unop_surjective`
`op_eq_bot` 📖	mathematical	—	`op` `Bot.bot` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instBot`	—	`op_injective` `op_bot`
`op_eq_top` 📖	mathematical	—	`op` `Top.top` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instTop`	—	`op_injective` `op_top`
`op_iInf` 📖	mathematical	—	`op` `iInf` `Subgroup` `instInfSet` `MulOpposite` `MulOpposite.instGroup`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `Subgroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instGroup`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `Subgroup` `instMin` `MulOpposite` `MulOpposite.instGroup`	—	—
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `Subgroup` `instInfSet` `MulOpposite` `MulOpposite.instGroup` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `Subgroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instGroup` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `MulOpposite` `MulOpposite.instGroup`	—	`OrderIso.map_sup`
`op_top` 📖	mathematical	—	`op` `Top.top` `Subgroup` `instTop` `MulOpposite` `MulOpposite.instGroup`	—	—
`smul_opposite_mul` 📖	mathematical	—	`MulOpposite` `Subgroup` `MulOpposite.instGroup` `SetLike.instMembership` `instSetLike` `op` `instSMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul_assoc`
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instBot`	—	`OrderIso.map_bot`
`unop_closure` 📖	mathematical	—	`unop` `closure` `MulOpposite` `MulOpposite.instGroup` `Set.preimage` `MulOpposite.op`	—	`op_unop` `op_closure` `Set.preimage_preimage`
`unop_eq_bot` 📖	mathematical	—	`unop` `Bot.bot` `Subgroup` `instBot` `MulOpposite` `MulOpposite.instGroup`	—	`unop_injective` `unop_bot`
`unop_eq_top` 📖	mathematical	—	`unop` `Top.top` `Subgroup` `instTop` `MulOpposite` `MulOpposite.instGroup`	—	`unop_injective` `unop_top`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instInfSet`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instMin`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instInfSet` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`OrderIso.map_sup`
`unop_top` 📖	mathematical	—	`unop` `Top.top` `Subgroup` `MulOpposite` `MulOpposite.instGroup` `instTop`	—	—

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_op` 📖	mathematical	—	`Subgroup.Normal`	—	`Subgroup.normal_op`
`of_unop` 📖	mathematical	—	`Subgroup.Normal` `MulOpposite` `MulOpposite.instGroup`	—	`Subgroup.normal_unop`
`op` 📖	mathematical	—	`Subgroup.Normal` `MulOpposite` `MulOpposite.instGroup` `Subgroup.op`	—	`Subgroup.normal_op`
`unop` 📖	mathematical	—	`Subgroup.Normal` `Subgroup.unop`	—	`Subgroup.normal_unop`

Subgroup.op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormal` 📖	mathematical	—	`Subgroup.Normal` `MulOpposite` `MulOpposite.instGroup` `Subgroup.op`	—	`Subgroup.Normal.op`

Subgroup.unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormal` 📖	mathematical	—	`Subgroup.Normal` `Subgroup.unop`	—	`Subgroup.Normal.unop`

---

← Back to Index