Documentation Verification Report

Int

📁 Source: Mathlib/Algebra/Module/LocalizedModule/Int.lean

Statistics

Metric	Count
Definitions `IsInteger`, `commonDenom`, `commonDenomOfFinset`, `finsetIntegerMultiple`, `integerMultiple`	5
Theorems `exist_integer_multiples`, `exist_integer_multiples_of_finite`, `exist_integer_multiples_of_finset`, `exists_integer_multiple`, `finsetIntegerMultiple_image`, `isInteger_add`, `isInteger_smul`, `isInteger_zero`, `map_integerMultiple`, `smul_mem_finsetIntegerMultiple_span`	10
Total	15

IsLocalizedModule

Definitions

Name	Category	Theorems
`IsInteger` 📖	MathDef	5 math math: `exist_integer_multiples`, `exist_integer_multiples_of_finset`, `exist_integer_multiples_of_finite`, `exists_integer_multiple`, `isInteger_zero`
`commonDenom` 📖	CompOp	1 math math: `map_integerMultiple`
`commonDenomOfFinset` 📖	CompOp	1 math math: `finsetIntegerMultiple_image`
`finsetIntegerMultiple` 📖	CompOp	2 math math: `finsetIntegerMultiple_image`, `smul_mem_finsetIntegerMultiple_span`
`integerMultiple` 📖	CompOp	1 math math: `map_integerMultiple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exist_integer_multiples` 📖	mathematical	—	`IsInteger` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `Submonoid.isScalarTower` `IsScalarTower.left` `Submonoid.coe_finset_prod` `SemigroupAction.mul_smul` `Submonoid.smul_def` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `mul_comm` `Finset.prod_insert` `Finset.notMem_erase` `Finset.insert_erase` `surj`
`exist_integer_multiples_of_finite` 📖	mathematical	—	`IsInteger` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`nonempty_fintype` `exist_integer_multiples` `Finset.mem_univ`
`exist_integer_multiples_of_finset` 📖	mathematical	—	`IsInteger` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`exist_integer_multiples`
`exists_integer_multiple` 📖	mathematical	—	`IsInteger` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`surj` `Set.mem_range`
`finsetIntegerMultiple_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SetLike.coe` `Finset` `Finset.instSetLike` `finsetIntegerMultiple` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Set` `Submonoid.smul` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `commonDenomOfFinset`	—	`Finset.coe_image` `Set.ext` `map_integerMultiple` `Set.mem_image_of_mem` `Subtype.prop` `Finset.mem_attach`
`isInteger_add` 📖	mathematical	`IsInteger`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Submodule.add_mem`
`isInteger_smul` 📖	mathematical	`IsInteger`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction`	—	`LinearMapClass.map_smul` `LinearMap.semilinearMapClass`
`isInteger_zero` 📖	mathematical	—	`IsInteger` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Submodule.zero_mem`
`map_integerMultiple` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `integerMultiple` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `commonDenom` `Finset` `Finset.instSetLike`	—	`exist_integer_multiples` `Subtype.prop`
`smul_mem_finsetIntegerMultiple_span` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Finset` `Finset.instSetLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`finsetIntegerMultiple` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`finsetIntegerMultiple_image` `smulCommClass_self` `Set.smul_mem_smul_set` `RingHomSurjective.ids` `Submodule.map_span` `LinearMap.map_smul` `Submonoid.smulCommClass_left` `Submodule.span_smul` `eq_iff_exists` `Submodule.smul_mem`

---

← Back to Index