Documentation Verification Report

Integer

📁 Source: Mathlib/RingTheory/Localization/Integer.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`, `exists_integer_multiple'`, `finsetIntegerMultiple_image`, `isInteger_add`, `isInteger_mul`, `isInteger_one`, `isInteger_smul`, `isInteger_zero`, `map_integerMultiple`	12
Total	17

IsLocalization

Definitions

Name	Category	Theorems
`IsInteger` 📖	MathDef	16 math math: `FractionalIdeal.isFractional_span_iff`, `ValuationRing.iff_isInteger_or_isInteger`, `UniqueFactorizationMonoid.integer_of_integral`, `isInteger_one`, `isInteger_of_is_root_of_monic`, `Rat.isLocalizationIsInteger_iff`, `exist_integer_multiples_of_finset`, `exist_integer_multiples_of_finite`, `IsFractionRing.isInteger_of_isUnit_den`, `isInteger_zero`, `exists_integer_multiple`, `exists_integer_multiple'`, `Ideal.exist_integer_multiples_notMem`, `ValuationRing.isInteger_or_isInteger`, `exist_integer_multiples`, `IsFractionRing.isUnit_den_iff`
`commonDenom` 📖	CompOp	2 math math: `map_integerMultiple`, `scaleRoots_commonDenom_mem_lifts`
`commonDenomOfFinset` 📖	CompOp	1 math math: `finsetIntegerMultiple_image`
`finsetIntegerMultiple` 📖	CompOp	3 math math: `smul_mem_finsetIntegerMultiple_span`, `lift_mem_adjoin_finsetIntegerMultiple`, `finsetIntegerMultiple_image`
`integerMultiple` 📖	CompOp	1 math math: `map_integerMultiple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exist_integer_multiples` 📖	mathematical	—	`IsInteger` `Algebra.toSMul` `CommSemiring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `sec_spec'` `mul_assoc` `RingHom.map_mul` `Algebra.smul_def` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `mul_comm` `Submonoid.coe_finset_prod` `Finset.prod_insert` `Finset.notMem_erase` `Finset.insert_erase` `map_prod` `MonoidHom.instMonoidHomClass`
`exist_integer_multiples_of_finite` 📖	mathematical	—	`IsInteger` `Algebra.toSMul` `CommSemiring.toSemiring` `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` `Algebra.toSMul` `CommSemiring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`exist_integer_multiples`
`exists_integer_multiple` 📖	mathematical	—	`IsInteger` `Algebra.toSMul` `CommSemiring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	—	`Algebra.smul_def` `mul_comm` `exists_integer_multiple'`
`exists_integer_multiple'` 📖	mathematical	—	`IsInteger` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`surj` `Set.mem_range`
`finsetIntegerMultiple_image` 📖	mathematical	—	`Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `SetLike.coe` `Finset` `Finset.instSetLike` `finsetIntegerMultiple` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Set` `Submonoid.smul` `Set.smulSet` `Algebra.toSMul` `commonDenomOfFinset`	—	`Finset.coe_image` `Set.ext` `map_integerMultiple` `Set.mem_image_of_mem` `Subtype.prop` `Finset.mem_attach`
`isInteger_add` 📖	mathematical	`IsInteger`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Subsemiring.add_mem`
`isInteger_mul` 📖	mathematical	`IsInteger`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Subsemiring.mul_mem`
`isInteger_one` 📖	mathematical	—	`IsInteger` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Subsemiring.one_mem`
`isInteger_smul` 📖	mathematical	`IsInteger`	`Algebra.toSMul` `CommSemiring.toSemiring`	—	`RingHom.map_mul` `Algebra.smul_def`
`isInteger_zero` 📖	mathematical	—	`IsInteger` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Subsemiring.zero_mem`
`map_integerMultiple` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `integerMultiple` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.smul` `Algebra.toSMul` `commonDenom` `Finset` `Finset.instSetLike`	—	`exist_integer_multiples` `Subtype.prop`

---

← Back to Index