Documentation Verification Report

MulAction

📁 Source: Mathlib/Algebra/Group/Submonoid/MulAction.lean

Statistics

Metric	Count
Definitions `addAction`, `instAddActionSubtypeMem`, `instVAddSubtypeMem`, `vadd`, `instMulActionSubtypeMem`, `instSMulSubtypeMem`, `mulAction`, `smul`	8
Theorems `instIsCancelVAddSubtypeMem`, `instIsLeftCancelVAddSubtypeMem`, `instVAddAssocClassSubtypeMem`, `instVAddCommClassSubtypeMem`, `instVAddCommClassSubtypeMem_1`, `mk_vadd`, `vaddAssocClass`, `vaddCommClass_left`, `vaddCommClass_right`, `vadd_def`, `instIsCancelSMulSubtypeMem`, `instIsLeftCancelSMulSubtypeMem`, `instIsScalarTowerSubtypeMem`, `instSMulCommClassSubtypeMem`, `instSMulCommClassSubtypeMem_1`, `isScalarTower`, `mk_smul`, `smulCommClass_left`, `smulCommClass_right`, `smul_def`	20
Total	28

AddSubmonoid

Definitions

Name	Category	Theorems
`addAction` 📖	CompOp	4 math math: `fixedPoints_addSubmonoid_iSup`, `fixingAddSubmonoid_fixedPoints_gc`, `fixedPoints_addSubmonoid_sup`, `fixedPoints_antitone_addSubmonoid`
`instAddActionSubtypeMem` 📖	CompOp	—
`instVAddSubtypeMem` 📖	CompOp	5 math math: `instIsCancelVAddSubtypeMem`, `instVAddCommClassSubtypeMem_1`, `instIsLeftCancelVAddSubtypeMem`, `instVAddCommClassSubtypeMem`, `instVAddAssocClassSubtypeMem`
`vadd` 📖	CompOp	14 math math: `continuousVAdd`, `Function.Periodic.map_vadd_multiples`, `MeasureTheory.Measure.instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant`, `AddOreLocalization.oreSub_eq_iff`, `AddAction.orbit_addSubmonoid_subset`, `vadd_def`, `vaddCommClass_left`, `instMeasurableConstVAdd`, `vaddAssocClass`, `faithfulVAdd`, `AddOreLocalization.expand'`, `instMeasurableVAdd`, `mk_vadd`, `vaddCommClass_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelVAddSubtypeMem` 📖	mathematical	—	`IsCancelVAdd` `SetLike.instMembership` `instVAddSubtypeMem`	—	`instIsLeftCancelVAddSubtypeMem` `IsCancelVAdd.toIsLeftCancelVAdd` `IsCancelVAdd.right_cancel`
`instIsLeftCancelVAddSubtypeMem` 📖	mathematical	—	`IsLeftCancelVAdd` `SetLike.instMembership` `instVAddSubtypeMem`	—	`IsLeftCancelVAdd.left_cancel`
`instVAddAssocClassSubtypeMem` 📖	mathematical	—	`VAddAssocClass` `SetLike.instMembership` `instVAddSubtypeMem`	—	`vadd_assoc`
`instVAddCommClassSubtypeMem` 📖	mathematical	—	`VAddCommClass` `SetLike.instMembership` `instVAddSubtypeMem`	—	`VAddCommClass.vadd_comm`
`instVAddCommClassSubtypeMem_1` 📖	mathematical	—	`VAddCommClass` `SetLike.instMembership` `instVAddSubtypeMem`	—	`VAddCommClass.vadd_comm`
`mk_vadd` 📖	mathematical	`AddSubmonoid` `SetLike.instMembership` `instSetLike`	`HVAdd.hVAdd` `instHVAdd` `vadd`	—	—
`vaddAssocClass` 📖	mathematical	—	`VAddAssocClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `vadd`	—	`instVAddAssocClassSubtypeMem`
`vaddCommClass_left` 📖	mathematical	—	`VAddCommClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `vadd`	—	`instVAddCommClassSubtypeMem`
`vaddCommClass_right` 📖	mathematical	—	`VAddCommClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `vadd`	—	`instVAddCommClassSubtypeMem_1`
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `instHVAdd` `vadd`	—	—

Submonoid

Definitions

Name	Category	Theorems
`instMulActionSubtypeMem` 📖	CompOp	4 math math: `AddSubgroup.subgroupOf_inertia`, `Subfield.continuousSMul`, `Subalgebra.inclusion.isScalarTower_right`, `AddSubgroup.inertia_map_subtype`
`instSMulSubtypeMem` 📖	CompOp	6 math math: `instIsCancelSMulSubtypeMem`, `Subsemiring.instFaithfulSMulSubtypeMem`, `instIsLeftCancelSMulSubtypeMem`, `instIsScalarTowerSubtypeMem`, `instSMulCommClassSubtypeMem_1`, `instSMulCommClassSubtypeMem`
`mulAction` 📖	CompOp	4 math math: `fixedPoints_submonoid_sup`, `fixedPoints_submonoid_iSup`, `fixingSubmonoid_fixedPoints_gc`, `fixedPoints_antitone`
`smul` 📖	CompOp	69 math math: `CStarRing.norm_unitary_smul`, `OreLocalization.oreDiv_add_char`, `IsLocalization.smul_mem_finsetIntegerMultiple_span`, `OreLocalization.oreDiv_eq_iff`, `isScalarTower`, `IsLocalization.lift_mem_adjoin_finsetIntegerMultiple`, `LocalizedModule.mk_add_mk`, `IsLocalizedModule.mk'_eq_zero'`, `Submodule.mem_torsion_iff`, `Submodule.isTorsion'_powers_iff`, `Unitary.smul_mem`, `instMeasurableSMul`, `LocalizedModule.mk_eq`, `IsLocalizedModule.mk'_add_mk'`, `LocalizedModule.mk_cancel`, `IsIntegral.exists_multiple_integral_of_isLocalization`, `IsLocalizedModule.mk'_eq_mk'_iff`, `unitary.coe_smul`, `IsLocalizedModule.finsetIntegerMultiple_image`, `Module.FinitePresentation.exists_lift_of_isLocalizedModule`, `multiple_mem_adjoin_of_mem_localization_adjoin`, `OreLocalization.expand'`, `IsLocalization.finsetIntegerMultiple_image`, `LocalizedModule.mk_cancel_common_left`, `AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux`, `isLocalizedModule_iff`, `unitary.smul_mem`, `OreLocalization.oreDiv_add_oreDiv`, `instSMulCommClassSubtypeMemCenter_1`, `mk_smul`, `IsLocalization.smul_bijective`, `Unitary.coe_smul`, `LocalizedModule.mk_cancel_common_right`, `instSMulCommClassSubtypeMemCenter`, `IsLocalizedModule.mk'_cancel'`, `IsLocalization.map_integerMultiple`, `faithfulSMul`, `Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule`, `smul_def`, `IsLocalizedModule.mk'_cancel_right`, `multiple_mem_span_of_mem_localization_span`, `IsLocalizedModule.smul_inj`, `IsLocalizedModule.iso_symm_apply_aux`, `center.smulCommClass_left`, `IsLocalizedModule.exists_of_eq`, `FractionalIdeal.den_mul_self_eq_num`, `smulCommClass_left`, `IsLocalization.exists_smul_mem_of_mem_adjoin`, `IsLocalization.smul_mem_iff`, `center.smulCommClass_right`, `continuousSMul`, `IsLocalizedModule.smul_injective`, `MulAction.orbit_submonoid_subset`, `instMeasurableConstSMul`, `MeasureTheory.Measure.instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant`, `smulCommClass_right`, `IsLocalizedModule.eq_iff_exists`, `FractionalIdeal.equivNum_apply`, `IsLocalizedModule.smul_mem_finsetIntegerMultiple_span`, `IsLocalizedModule.map_integerMultiple`, `IsLocalizedModule.mk'_cancel`, `IsLocalizedModule.mk'_cancel_left`, `IsLocalizedModule.mk'_eq_iff`, `IsLocalization.smul_toInvSubmonoid`, `IsLocalizedModule.eq_zero_iff`, `IsLocalizedModule.surj'`, `IsLocalizedModule.surj`, `IsLocalizedModule.mk'_sub_mk'`, `IsLocalizedModule.injective_iff_isRegular`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelSMulSubtypeMem` 📖	mathematical	—	`IsCancelSMul` `SetLike.instMembership` `instSMulSubtypeMem`	—	`instIsLeftCancelSMulSubtypeMem` `IsCancelSMul.toIsLeftCancelSMul` `IsCancelSMul.right_cancel`
`instIsLeftCancelSMulSubtypeMem` 📖	mathematical	—	`IsLeftCancelSMul` `SetLike.instMembership` `instSMulSubtypeMem`	—	`IsLeftCancelSMul.left_cancel`
`instIsScalarTowerSubtypeMem` 📖	mathematical	—	`IsScalarTower` `SetLike.instMembership` `instSMulSubtypeMem`	—	`smul_assoc`
`instSMulCommClassSubtypeMem` 📖	mathematical	—	`SMulCommClass` `SetLike.instMembership` `instSMulSubtypeMem`	—	`SMulCommClass.smul_comm`
`instSMulCommClassSubtypeMem_1` 📖	mathematical	—	`SMulCommClass` `SetLike.instMembership` `instSMulSubtypeMem`	—	`SMulCommClass.smul_comm`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Submonoid` `SetLike.instMembership` `instSetLike` `smul`	—	`instIsScalarTowerSubtypeMem`
`mk_smul` 📖	mathematical	`Submonoid` `SetLike.instMembership` `instSetLike`	`smul`	—	—
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Submonoid` `SetLike.instMembership` `instSetLike` `smul`	—	`instSMulCommClassSubtypeMem`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Submonoid` `SetLike.instMembership` `instSetLike` `smul`	—	`instSMulCommClassSubtypeMem_1`
`smul_def` 📖	mathematical	—	`Submonoid` `SetLike.instMembership` `instSetLike` `smul`	—	—

---

← Back to Index