Basic

📁 Source: Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

Statistics

Metric	Count
Definitions `DomAddAct`, `instAddActionForall`, `instAddCancelCommMonoidOfAddOpposite`, `instAddCancelMonoidOfAddOpposite`, `instAddCommGroupOfAddOpposite`, `instAddCommMonoidOfAddOpposite`, `instAddCommSemigroupOfAddOpposite`, `instAddGroupOfAddOpposite`, `instAddLeftCancelMonoidOfAddOpposite`, `instAddLeftCancelSemigroupOfAddOpposite`, `instAddMonoidOfAddOpposite`, `instAddOfAddOpposite`, `instAddRightCancelMonoidOfAddOpposite`, `instAddRightCancelSemigroupOfAddOpposite`, `instAddSemigroupOfAddOpposite`, `instAddZeroClassOfAddOpposite`, `instCommRingOfAddOpposite`, `instDivisionAddCommMonoidOfAddOpposite`, `instInvolutiveNegOfAddOpposite`, `instNegOfAddOpposite`, `instNegZeroClassOfAddOpposite`, `instNonAssocSemiringOfAddOpposite`, `instNonUnitalSemiringOfAddOpposite`, `instRingOfAddOpposite`, `instSemiringOfAddOpposite`, `instSubNegAddMonoidOfAddOpposite`, `instSubNegZeroMonoidOfAddOpposite`, `instSubtractionMonoidOfAddOpposite`, `instVAddForall`, `instZeroOfAddOpposite`, `mk`, `instCancelCommMonoidOfMulOpposite`, `instCancelMonoidOfMulOpposite`, `instCommGroupOfMulOpposite`, `instCommMonoidOfMulOpposite`, `instCommRingOfMulOpposite`, `instCommSemigroupOfMulOpposite`, `instDistribMulActionAddMonoidHom`, `instDistribMulActionForallOfMulAction`, `instDistribSMulForallOfSMul`, `instDivInvMonoidOfMulOpposite`, `instDivInvOneMonoidOfMulOpposite`, `instDivisionCommMonoidOfMulOpposite`, `instDivisionMonoidOfMulOpposite`, `instGroupOfMulOpposite`, `instInvOfMulOpposite`, `instInvOneClassOfMulOpposite`, `instInvolutiveInvOfMulOpposite`, `instLeftCancelMonoidOfMulOpposite`, `instLeftCancelSemigroupOfMulOpposite`, `instMonoidOfMulOpposite`, `instMulActionAddMonoidHomOfDistribMulAction`, `instMulActionForall`, `instMulActionMonoidHom`, `instMulDistribMulActionForallOfMulAction`, `instMulDistribMulActionMonoidHom`, `instMulOfMulOpposite`, `instMulOneClassOfMulOpposite`, `instNonAssocSemiringOfMulOpposite`, `instNonUnitalSemiringOfMulOpposite`, `instOneOfMulOpposite`, `instRightCancelMonoidOfMulOpposite`, `instRightCancelSemigroupOfMulOpposite`, `instRingOfMulOpposite`, `instSMulAddMonoidHom`, `instSMulForall`, `instSMulMonoidHom`, `instSMulZeroClassForallOfSMul`, `instSemigroupOfMulOpposite`, `instSemiringOfMulOpposite`, `mk`, `«term_ᵈᵃᵃ»`, `«term_ᵈᵐᵃ»`	73
Theorems `instFaithfulVAddForallOfNontrivial`, `instIsCancelAddOfAddOpposite`, `instIsLeftCancelAddOfAddOpposite`, `instIsRightCancelAddOfAddOpposite`, `instVAddCommClassForall`, `instVAddCommClassForall_1`, `instVAddCommClassForall_2`, `mk_add`, `mk_neg`, `mk_nsmul`, `mk_zero`, `mk_zsmul`, `symm_mk_add`, `symm_mk_neg`, `symm_mk_nsmul`, `symm_mk_zero`, `symm_mk_zsmul`, `vadd_apply`, `coe_smul_addMonoidHom`, `instFaithfulSMulForallOfNontrivial`, `instIsCancelMulOfMulOpposite`, `instIsLeftCancelMulOfMulOpposite`, `instIsRightCancelMulOfMulOpposite`, `instSMulCommClassAddMonoidHom`, `instSMulCommClassAddMonoidHom_1`, `instSMulCommClassForall`, `instSMulCommClassForall_1`, `instSMulCommClassForall_2`, `instSMulCommClassMonoidHom`, `mk_inv`, `mk_mul`, `mk_one`, `mk_pow`, `mk_smul_addMonoidHom_apply`, `mk_smul_monoidHom_apply`, `mk_zpow`, `smul_addMonoidHom_apply`, `smul_apply`, `smul_monoidHom_apply`, `symm_mk_inv`, `symm_mk_mul`, `symm_mk_one`, `symm_mk_pow`, `symm_mk_zpow`	44
Total	117

DomAddAct

Definitions

Name	Category	Theorems
`instAddActionForall` 📖	CompOp	—
`instAddCancelCommMonoidOfAddOpposite` 📖	CompOp	—
`instAddCancelMonoidOfAddOpposite` 📖	CompOp	—
`instAddCommGroupOfAddOpposite` 📖	CompOp	—
`instAddCommMonoidOfAddOpposite` 📖	CompOp	—
`instAddCommSemigroupOfAddOpposite` 📖	CompOp	—
`instAddGroupOfAddOpposite` 📖	CompOp	—
`instAddLeftCancelMonoidOfAddOpposite` 📖	CompOp	—
`instAddLeftCancelSemigroupOfAddOpposite` 📖	CompOp	—
`instAddMonoidOfAddOpposite` 📖	CompOp	2 math math: `mk_nsmul`, `symm_mk_nsmul`
`instAddOfAddOpposite` 📖	CompOp	5 math math: `instIsLeftCancelAddOfAddOpposite`, `symm_mk_add`, `instIsCancelAddOfAddOpposite`, `mk_add`, `instIsRightCancelAddOfAddOpposite`
`instAddRightCancelMonoidOfAddOpposite` 📖	CompOp	—
`instAddRightCancelSemigroupOfAddOpposite` 📖	CompOp	—
`instAddSemigroupOfAddOpposite` 📖	CompOp	—
`instAddZeroClassOfAddOpposite` 📖	CompOp	—
`instCommRingOfAddOpposite` 📖	CompOp	—
`instDivisionAddCommMonoidOfAddOpposite` 📖	CompOp	—
`instInvolutiveNegOfAddOpposite` 📖	CompOp	—
`instNegOfAddOpposite` 📖	CompOp	2 math math: `symm_mk_neg`, `mk_neg`
`instNegZeroClassOfAddOpposite` 📖	CompOp	—
`instNonAssocSemiringOfAddOpposite` 📖	CompOp	—
`instNonUnitalSemiringOfAddOpposite` 📖	CompOp	—
`instRingOfAddOpposite` 📖	CompOp	—
`instSemiringOfAddOpposite` 📖	CompOp	—
`instSubNegAddMonoidOfAddOpposite` 📖	CompOp	2 math math: `mk_zsmul`, `symm_mk_zsmul`
`instSubNegZeroMonoidOfAddOpposite` 📖	CompOp	—
`instSubtractionMonoidOfAddOpposite` 📖	CompOp	—
`instVAddForall` 📖	CompOp	6 math math: `instVAddCommClassForall_1`, `instVAddCommClassForall_2`, `instVAddCommClassForall`, `translate_eq_domAddActMk_vadd`, `instFaithfulVAddForallOfNontrivial`, `vadd_apply`
`instZeroOfAddOpposite` 📖	CompOp	2 math math: `mk_zero`, `symm_mk_zero`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulVAddForallOfNontrivial` 📖	mathematical	—	`FaithfulVAdd` `DomAddAct` `instVAddForall`	—	`Equiv.injective` `FaithfulVAdd.eq_of_vadd_eq_vadd` `exists_pair_ne` `Mathlib.Tactic.Contrapose.contrapose₂` `Function.update_of_ne` `Function.update_self`
`instIsCancelAddOfAddOpposite` 📖	mathematical	—	`IsCancelAdd` `DomAddAct` `instAddOfAddOpposite`	—	—
`instIsLeftCancelAddOfAddOpposite` 📖	mathematical	—	`IsLeftCancelAdd` `DomAddAct` `instAddOfAddOpposite`	—	—
`instIsRightCancelAddOfAddOpposite` 📖	mathematical	—	`IsRightCancelAdd` `DomAddAct` `instAddOfAddOpposite`	—	—
`instVAddCommClassForall` 📖	mathematical	—	`VAddCommClass` `DomAddAct` `instVAddForall` `Pi.instVAdd`	—	—
`instVAddCommClassForall_1` 📖	mathematical	—	`VAddCommClass` `DomAddAct` `Pi.instVAdd` `instVAddForall`	—	—
`instVAddCommClassForall_2` 📖	mathematical	—	`VAddCommClass` `DomAddAct` `instVAddForall`	—	`VAddCommClass.vadd_comm`
`mk_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instAddOfAddOpposite` `AddOpposite.instAdd`	—	—
`mk_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instNegOfAddOpposite` `AddOpposite.instNeg`	—	—
`mk_nsmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddMonoid.toNatSMul` `instAddMonoidOfAddOpposite` `AddOpposite.instAddMonoid`	—	—
`mk_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instZeroOfAddOpposite` `AddOpposite.instZero`	—	—
`mk_zsmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `SubNegMonoid.toZSMul` `instSubNegAddMonoidOfAddOpposite` `AddOpposite.instSubNegMonoid`	—	—
`symm_mk_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instAddOfAddOpposite` `AddOpposite.instAdd`	—	—
`symm_mk_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instNegOfAddOpposite` `AddOpposite.instNeg`	—	—
`symm_mk_nsmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `AddMonoid.toNatSMul` `instAddMonoidOfAddOpposite` `AddOpposite.instAddMonoid`	—	—
`symm_mk_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instZeroOfAddOpposite` `AddOpposite.instZero`	—	—
`symm_mk_zsmul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomAddAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `SubNegMonoid.toZSMul` `instSubNegAddMonoidOfAddOpposite` `AddOpposite.instSubNegMonoid`	—	—
`vadd_apply` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddForall` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—

DomMulAct

Definitions

Name	Category	Theorems
`instCancelCommMonoidOfMulOpposite` 📖	CompOp	—
`instCancelMonoidOfMulOpposite` 📖	CompOp	—
`instCommGroupOfMulOpposite` 📖	CompOp	—
`instCommMonoidOfMulOpposite` 📖	CompOp	—
`instCommRingOfMulOpposite` 📖	CompOp	—
`instCommSemigroupOfMulOpposite` 📖	CompOp	—
`instDistribMulActionAddMonoidHom` 📖	CompOp	—
`instDistribMulActionForallOfMulAction` 📖	CompOp	—
`instDistribSMulForallOfSMul` 📖	CompOp	—
`instDivInvMonoidOfMulOpposite` 📖	CompOp	2 math math: `mk_zpow`, `symm_mk_zpow`
`instDivInvOneMonoidOfMulOpposite` 📖	CompOp	—
`instDivisionCommMonoidOfMulOpposite` 📖	CompOp	—
`instDivisionMonoidOfMulOpposite` 📖	CompOp	—
`instGroupOfMulOpposite` 📖	CompOp	2 math math: `mem_stabilizer_iff`, `stabilizerMulEquiv_apply`
`instInvOfMulOpposite` 📖	CompOp	3 math math: `MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar`, `mk_inv`, `symm_mk_inv`
`instInvOneClassOfMulOpposite` 📖	CompOp	—
`instInvolutiveInvOfMulOpposite` 📖	CompOp	—
`instLeftCancelMonoidOfMulOpposite` 📖	CompOp	—
`instLeftCancelSemigroupOfMulOpposite` 📖	CompOp	—
`instMonoidOfMulOpposite` 📖	CompOp	15 math math: `MeasureTheory.integral_domSMul`, `MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar`, `symm_mk_pow`, `MeasureTheory.Measure.domSMul_apply`, `MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv`, `MeasureTheory.Measure.IsAddHaarMeasure.domSMul`, `MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar`, `MeasureTheory.Measure.addHaarScalarFactor_smul_congr`, `MeasureTheory.distribHaarChar_apply`, `MeasureTheory.Measure.Regular.domSMul`, `MeasureTheory.Measure.instSMulCommClassDomMulActNNReal`, `MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct`, `mk_pow`, `MeasureTheory.Measure.addHaarScalarFactor_domSMul`, `MeasureTheory.Measure.addHaarScalarFactor_smul_congr'`
`instMulActionAddMonoidHomOfDistribMulAction` 📖	CompOp	—
`instMulActionForall` 📖	CompOp	2 math math: `mem_stabilizer_iff`, `stabilizerMulEquiv_apply`
`instMulActionMonoidHom` 📖	CompOp	—
`instMulDistribMulActionForallOfMulAction` 📖	CompOp	—
`instMulDistribMulActionMonoidHom` 📖	CompOp	—
`instMulOfMulOpposite` 📖	CompOp	5 math math: `instIsCancelMulOfMulOpposite`, `instIsLeftCancelMulOfMulOpposite`, `mk_mul`, `instIsRightCancelMulOfMulOpposite`, `symm_mk_mul`
`instMulOneClassOfMulOpposite` 📖	CompOp	—
`instNonAssocSemiringOfMulOpposite` 📖	CompOp	2 math math: `LinearEquiv.domMulActCongrRight_symm_apply`, `LinearEquiv.domMulActCongrRight_apply`
`instNonUnitalSemiringOfMulOpposite` 📖	CompOp	—
`instOneOfMulOpposite` 📖	CompOp	2 math math: `symm_mk_one`, `mk_one`
`instRightCancelMonoidOfMulOpposite` 📖	CompOp	—
`instRightCancelSemigroupOfMulOpposite` 📖	CompOp	—
`instRingOfMulOpposite` 📖	CompOp	—
`instSMulAddMonoidHom` 📖	CompOp	5 math math: `smul_addMonoidHom_apply`, `coe_smul_addMonoidHom`, `instSMulCommClassAddMonoidHom`, `instSMulCommClassAddMonoidHom_1`, `mk_smul_addMonoidHom_apply`
`instSMulForall` 📖	CompOp	7 math math: `instFaithfulSMulForallOfNontrivial`, `coe_smul_addMonoidHom`, `instSMulCommClassForall_1`, `coe_smul_linearMap`, `instSMulCommClassForall_2`, `instSMulCommClassForall`, `smul_apply`
`instSMulMonoidHom` 📖	CompOp	3 math math: `smul_monoidHom_apply`, `instSMulCommClassMonoidHom`, `mk_smul_monoidHom_apply`
`instSMulZeroClassForallOfSMul` 📖	CompOp	—
`instSemigroupOfMulOpposite` 📖	CompOp	—
`instSemiringOfMulOpposite` 📖	CompOp	2 math math: `LinearEquiv.domMulActCongrRight_symm_apply`, `LinearEquiv.domMulActCongrRight_apply`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul_addMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `DomMulAct` `instSMulAddMonoidHom` `instSMulForall` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass`	—	—
`instFaithfulSMulForallOfNontrivial` 📖	mathematical	—	`FaithfulSMul` `DomMulAct` `instSMulForall`	—	`Equiv.injective` `FaithfulSMul.eq_of_smul_eq_smul` `exists_pair_ne` `Mathlib.Tactic.Contrapose.contrapose₂` `Function.update_of_ne` `Function.update_self`
`instIsCancelMulOfMulOpposite` 📖	mathematical	—	`IsCancelMul` `DomMulAct` `instMulOfMulOpposite`	—	—
`instIsLeftCancelMulOfMulOpposite` 📖	mathematical	—	`IsLeftCancelMul` `DomMulAct` `instMulOfMulOpposite`	—	—
`instIsRightCancelMulOfMulOpposite` 📖	mathematical	—	`IsRightCancelMul` `DomMulAct` `instMulOfMulOpposite`	—	—
`instSMulCommClassAddMonoidHom` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instSMulAddMonoidHom`	—	`Function.Injective.smulCommClass` `instSMulCommClassForall_2` `DFunLike.coe_injective`
`instSMulCommClassAddMonoidHom_1` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instSMulAddMonoidHom` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `AddMonoidHom.instSMulZeroClassOfDistribSMul`	—	`Function.Injective.smulCommClass` `instSMulCommClassForall` `DFunLike.coe_injective`
`instSMulCommClassForall` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `instSMulForall` `Pi.instSMul`	—	—
`instSMulCommClassForall_1` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `Pi.instSMul` `instSMulForall`	—	—
`instSMulCommClassForall_2` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `instSMulForall`	—	`SMulCommClass.smul_comm`
`instSMulCommClassMonoidHom` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instSMulMonoidHom`	—	`Function.Injective.smulCommClass` `instSMulCommClassForall_2` `DFunLike.coe_injective`
`mk_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instInvOfMulOpposite` `MulOpposite.instInv`	—	—
`mk_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instMulOfMulOpposite` `MulOpposite.instMul`	—	—
`mk_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `instOneOfMulOpposite` `MulOpposite.instOne`	—	—
`mk_pow` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Monoid.toNatPow` `instMonoidOfMulOpposite` `MulOpposite.instMonoid`	—	—
`mk_smul_addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `DomMulAct` `instSMulAddMonoidHom` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass`	—	—
`mk_smul_monoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `DomMulAct` `instSMulMonoidHom` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction`	—	—
`mk_zpow` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `instDivInvMonoidOfMulOpposite` `MulOpposite.instDivInvMonoid`	—	—
`smul_addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `DomMulAct` `instSMulAddMonoidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`smul_apply` 📖	mathematical	—	`DomMulAct` `instSMulForall` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`smul_monoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `DomMulAct` `instSMulMonoidHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`symm_mk_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instInvOfMulOpposite` `MulOpposite.instInv`	—	—
`symm_mk_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instMulOfMulOpposite` `MulOpposite.instMul`	—	—
`symm_mk_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `instOneOfMulOpposite` `MulOpposite.instOne`	—	—
`symm_mk_pow` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Monoid.toNatPow` `instMonoidOfMulOpposite` `MulOpposite.instMonoid`	—	—
`symm_mk_zpow` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DomMulAct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `DivInvMonoid.toZPow` `instDivInvMonoidOfMulOpposite` `MulOpposite.instDivInvMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`DomAddAct` 📖	CompOp	76 math math: `DomAddAct.instSecondCountableTopology`, `DomAddAct.mk_vadd_indicatorConstLp`, `DomAddAct.instT3Space`, `DomAddAct.instIsLeftCancelAddOfAddOpposite`, `DomAddAct.instVAddCommClassAEEqFun_2`, `DomAddAct.map_mk_symm_nhds`, `DomAddAct.instVAddCommClassForall_1`, `DomAddAct.isOpenEmbedding_mk`, `DomAddAct.instT4Space`, `DomAddAct.isOpenEmbedding_mk_symm`, `DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp`, `DomAddAct.vadd_Lp_add`, `DomAddAct.isInducing_mk`, `DomAddAct.continuous_mk_symm`, `DomAddAct.instCompactSpace`, `DomAddAct.symm_mk_neg`, `DomAddAct.symm_mk_add`, `DomAddAct.mk_zsmul`, `DomAddAct.instCompletelyNormalSpace`, `DomAddAct.instVAddCommClassForall_2`, `DomAddAct.comap_mk.symm_nhds`, `DomAddAct.instIsCancelAddOfAddOpposite`, `DomAddAct.symm_mk_zsmul`, `DomAddAct.norm_vadd_Lp`, `DomAddAct.instLocallyCompactSpace`, `DomAddAct.mk_add`, `DomAddAct.vadd_aeeqFun_const`, `DomAddAct.instVAddCommClassForall`, `DomAddAct.vadd_aeeqFun_aeeq`, `DomAddAct.vadd_Lp_ae_eq`, `DomAddAct.vadd_Lp_sub`, `MeasureTheory.Lp.instContinuousVAddDomAddAct`, `translate_eq_domAddActMk_vadd`, `DomAddAct.instDiscreteTopology`, `DomAddAct.instT0Space`, `DomAddAct.vadd_Lp_neg`, `DomAddAct.continuous_mk`, `DomAddAct.instR0Space`, `DomAddAct.isQuotientMap_mk_symm`, `DomAddAct.edist_vadd_Lp`, `DomAddAct.instR1Space`, `DomAddAct.mk_nsmul`, `DomAddAct.instFaithfulVAddForallOfNontrivial`, `DomAddAct.mk_vadd_toLp`, `DomAddAct.instT5Space`, `DomAddAct.vadd_Lp_const`, `DomAddAct.isEmbedding_mk`, `DomAddAct.instRegularSpace`, `DomAddAct.coe_mkHomeomorph_symm`, `DomAddAct.toEquiv_mkHomeomorph`, `DomAddAct.mk_neg`, `DomAddAct.map_mk_nhds`, `DomAddAct.instT1Space`, `DomAddAct.coe_mkHomeomorph`, `DomAddAct.mk_vadd_mk_aeeqFun`, `DomAddAct.symm_mk_nsmul`, `DomAddAct.mk_zero`, `DomAddAct.instT25Space`, `DomAddAct.instIsRightCancelAddOfAddOpposite`, `DomAddAct.instSeparableSpace`, `DomAddAct.vadd_apply`, `DomAddAct.isClosedEmbedding_mk`, `DomAddAct.instFirstCountableTopology`, `DomAddAct.dist_vadd_Lp`, `DomAddAct.vadd_Lp_zero`, `DomAddAct.isEmbedding_mk_symm`, `DomAddAct.isClosedEmbedding_mk_symm`, `DomAddAct.nnnorm_vadd_Lp`, `DomAddAct.isQuotientMap_mk`, `DomAddAct.comap_mk_nhds`, `DomAddAct.symm_mk_zero`, `DomAddAct.instNormalSpace`, `DomAddAct.vadd_Lp_val`, `DomAddAct.instWeaklyLocallyCompactSpace`, `DomAddAct.isInducing_mk_symm`, `DomAddAct.instT2Space`
`«term_ᵈᵃᵃ»` 📖	CompOp	—
`«term_ᵈᵐᵃ»` 📖	CompOp	—

---

← Back to Index