Opposite

📁 Source: Mathlib/Algebra/Group/Action/Opposite.lean

Statistics

Metric	Count
Definitions toOppositeAddAction, instAddAction, toOppositeMulAction, instMulAction, «term_+ᵥ>_», «term_<+ᵥ_», «term_<•_», «term_•>_»	8
Theorems isCentralVAdd, instIsCentralVAdd, instVAddAssocClass, instVAddCommClass, op_vadd_eq_op_vadd_op, unop_vadd_eq_unop_vadd_unop, opposite_vaddCommClass, opposite_vaddCommClass', isCentralScalar, opposite_mid, instIsCentralScalar, instIsScalarTower, instSMulCommClass, op_smul_eq_op_smul_op, unop_smul_eq_unop_smul_unop, opposite_mid, opposite_smulCommClass, opposite_smulCommClass', opposite_mid, opposite_mid, op_smul_mul, op_smul_op_smul, op_vadd_add, op_vadd_op_vadd	24
Total	32

AddCommSemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCentralVAdd 📖	mathematical	—	IsCentralVAdd Add.toVAdd AddCommMagma.toAdd toAddCommMagma Add.toVAddAddOpposite	—	add_comm

AddMonoid

Definitions

Name	Category	Theorems
toOppositeAddAction 📖	CompOp	39 math math: AddSubgroup.vadd_opposite_image_add_preimage', rightAddCoset_zero, Finset.neg_op_vadd_finset_distrib, rightAddCoset_mem_rightAddCoset, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp, Finset.op_vadd_stabilizer_of_no_doubling, MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set, Set.neg_op_vadd_set_distrib, AddAction.stabilizer_op_addSubgroup, instErgodicVAddAddOppositeOfIsAddRightInvariant, op_vadd_coe_set, mem_rightAddCoset_iff, NormedAddGroup.to_isIsometricVAdd_right, AddSubgroup.isAddQuotientCoveringMap, rightAddCoset_eq_iff, instProperVAddAddOppositeOfIsTopologicalAddGroup, AddAction.op_vadd_set_stabilizer_subset, eq_addCosets_of_normal, Set.op_vadd_inter_nonempty_iff, Finset.op_vadd_addConvolution_eq_addConvolution_vadd, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, QuotientAddGroup.orbit_eq_out_vadd, mem_own_rightAddCoset, AddAction.right_quotientAction, Finset.addETransformLeft_fst, Set.neg_vadd_set_distrib, orbit_addSubgroup_eq_rightCoset, normal_iff_eq_addCosets, instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe, Finset.addConvolution_op_vadd_eq_addConvolution_add_neg, IsOpen.right_addCoset, IsClosed.right_addCoset, AddAction.right_quotientAction', Finset.addETransformRight_fst, QuotientAddGroup.orbit_mk_eq_vadd, Finset.neg_vadd_finset_distrib, MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure

AddOpposite

Definitions

Name	Category	Theorems
instAddAction 📖	CompOp	1 math math: AddAction.stabilizer_addSubgroup_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCentralVAdd 📖	mathematical	—	IsCentralVAdd AddOpposite instVAdd	—	unop_injective IsCentralVAdd.op_vadd_eq_vadd
instVAddAssocClass 📖	mathematical	—	VAddAssocClass AddOpposite instVAdd	—	unop_injective vadd_assoc
instVAddCommClass 📖	mathematical	—	VAddCommClass AddOpposite instVAdd	—	unop_injective VAddCommClass.vadd_comm
op_vadd_eq_op_vadd_op 📖	mathematical	—	op HVAdd.hVAdd instHVAdd AddOpposite instVAdd	—	IsCentralVAdd.op_vadd_eq_vadd instIsCentralVAdd
unop_vadd_eq_unop_vadd_unop 📖	mathematical	—	unop HVAdd.hVAdd AddOpposite instHVAdd instVAdd	—	IsCentralVAdd.unop_vadd_eq_vadd

AddSemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_vaddCommClass 📖	mathematical	—	VAddCommClass AddOpposite Add.toVAddAddOpposite toAdd Add.toVAdd	—	add_assoc
opposite_vaddCommClass' 📖	mathematical	—	VAddCommClass AddOpposite Add.toVAdd toAdd Add.toVAddAddOpposite	—	VAddCommClass.symm opposite_vaddCommClass

CommSemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCentralScalar 📖	mathematical	—	IsCentralScalar CommMagma.toMul toCommMagma Mul.toSMulMulOpposite	—	mul_comm

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_mid 📖	mathematical	—	IsScalarTower MulOpposite MulOpposite.instSMul Mul.toSMulMulOpposite	—	mul_smul_comm

Monoid

Definitions

Name	Category	Theorems
toOppositeMulAction 📖	CompOp	46 math math: DoubleCoset.doubleCoset_union_rightCoset, NormedGroup.to_isIsometricSMul_right, mem_own_rightCoset, MulAction.right_quotientAction', Finset.inv_smul_finset_distrib, Finset.doubling_lt_three_halves, MulAction.right_quotientAction, Finset.inv_op_smul_finset_distrib, rightCoset_eq_iff, MulAction.op_smul_set_stabilizer_subset, Finset.smul_inv_mul_eq_inv_mul_opSMul, Subgroup.smul_diff_smul', Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp, op_smul_coe_set, MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set, normal_iff_eq_cosets, Set.op_smul_inter_nonempty_iff, MulAction.stabilizer_op_subgroup, QuotientGroup.orbit_eq_out_smul, Set.inv_smul_set_distrib, IsOpen.rightCoset, rightCoset_mem_rightCoset, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure, Finset.op_smul_convolution_eq_convolution_smul, Subgroup.smul_opposite_image_mul_preimage', StarSemigroup.toOpposite_starModule, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, Finset.mulETransformRight_fst, orbit_subgroup_eq_rightCoset, Set.inv_op_smul_set_distrib, instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe, instProperSMulMulOppositeOfIsTopologicalGroup, instErgodicSMulMulOppositeOfIsMulRightInvariant, QuotientGroup.orbit_mk_eq_smul, eq_cosets_of_normal, Finset.op_smul_stabilizer_of_no_doubling, rightCoset_one, MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage, mem_rightCoset_iff, Subgroup.smul_diff', Finset.mulETransformLeft_fst, TrivSqZeroExt.mul_inl_eq_op_smul, Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves, Subgroup.isQuotientCoveringMap, IsClosed.rightCoset, Finset.convolution_op_smul_eq_convolution_mul_inv

MulOpposite

Definitions

Name	Category	Theorems
instMulAction 📖	CompOp	1 math math: MulAction.stabilizer_subgroup_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCentralScalar 📖	mathematical	—	IsCentralScalar MulOpposite instSMul	—	unop_injective IsCentralScalar.op_smul_eq_smul
instIsScalarTower 📖	mathematical	—	IsScalarTower MulOpposite instSMul	—	unop_injective smul_assoc
instSMulCommClass 📖	mathematical	—	SMulCommClass MulOpposite instSMul	—	unop_injective SMulCommClass.smul_comm
op_smul_eq_op_smul_op 📖	mathematical	—	op MulOpposite instSMul	—	IsCentralScalar.op_smul_eq_smul instIsCentralScalar
unop_smul_eq_unop_smul_unop 📖	mathematical	—	unop MulOpposite instSMul	—	IsCentralScalar.unop_smul_eq_smul

RightActions

Definitions

Name	Category	Theorems
«term_+ᵥ>_» 📖	CompOp	—
«term_<+ᵥ_» 📖	CompOp	—
«term_<•_» 📖	CompOp	—
«term_•>_» 📖	CompOp	—

SMulCommClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_mid 📖	mathematical	—	SMulCommClass MulOpposite Mul.toSMulMulOpposite	—	smul_mul_assoc

Semigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_smulCommClass 📖	mathematical	—	SMulCommClass MulOpposite Mul.toSMulMulOpposite toMul	—	mul_assoc
opposite_smulCommClass' 📖	mathematical	—	SMulCommClass MulOpposite toMul Mul.toSMulMulOpposite	—	SMulCommClass.symm opposite_smulCommClass

VAddAssocClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_mid 📖	mathematical	—	VAddAssocClass AddOpposite AddOpposite.instVAdd Add.toVAddAddOpposite	—	add_vadd_comm

VAddCommClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opposite_mid 📖	mathematical	—	VAddCommClass AddOpposite Add.toVAddAddOpposite	—	vadd_add_assoc

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_smul_mul 📖	mathematical	—	MulOpposite SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid MulAction.toSemigroupAction MulOpposite.op MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	SemigroupAction.mul_smul
op_smul_op_smul 📖	mathematical	—	MulOpposite SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid MulAction.toSemigroupAction MulOpposite.op MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	smul_smul
op_vadd_add 📖	mathematical	—	HVAdd.hVAdd AddOpposite instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid AddAction.toAddSemigroupAction AddOpposite.op AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	AddSemigroupAction.add_vadd
op_vadd_op_vadd 📖	mathematical	—	HVAdd.hVAdd AddOpposite instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid AddAction.toAddSemigroupAction AddOpposite.op AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	vadd_vadd

---

← Back to Index