Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Squarefree/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `squarefree_iff`, `squarefree_prod_of_pairwise_isCoprime`, `squarefree_natAbs`, `squarefree_natCast`, `squarefree`, `squarefree`, `of_squarefree_mul`, `squarefree`, `squarefree`, `dvd_of_squarefree_of_mul_dvd_mul_left`, `dvd_of_squarefree_of_mul_dvd_mul_right`, `dvd_pow_iff_dvd`, `eq_zero_or_one_of_pow_of_not_isUnit`, `gcd_left`, `gcd_right`, `isRadical`, `ne_zero`, `of_mul_left`, `of_mul_right`, `pow_dvd_of_pow_dvd`, `pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left`, `pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right`, `squarefree_of_dvd`, `squarefree_iff_nodup_normalizedFactors`, `exists_squarefree_dvd_pow_of_ne_zero`, `irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree`, `isRadical_iff_squarefree_of_ne_zero`, `isRadical_iff_squarefree_or_zero`, `not_squarefree_zero`, `squarefree_iff_emultiplicity_le_one`, `squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible`, `squarefree_iff_irreducible_sq_not_dvd_of_ne_zero`, `squarefree_iff_no_irreducibles`, `squarefree_mul_iff`, `squarefree_one`	35
Total	35

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree_iff` 📖	mathematical	`Associated`	`Squarefree`	—	`Squarefree.squarefree_of_dvd` `dvd'` `dvd`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree_prod_of_pairwise_isCoprime` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Squarefree`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `prod` `CommMonoidWithZero.toCommMonoid`	—	`cons_induction` `prod_cons` `squarefree_mul_iff` `IsRelPrime.prod_right` `Set.pairwise_insert` `coe_cons` `mem_cons_of_mem`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree_natAbs` 📖	mathematical	—	`Squarefree` `Nat.instMonoid` `instMonoid`	—	`Function.Surjective.forall` `natAbs_surjective`
`squarefree_natCast` 📖	mathematical	—	`Squarefree` `instMonoid` `Nat.instMonoid`	—	`squarefree_natAbs`

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree` 📖	mathematical	`Irreducible` `CommMonoid.toMonoid`	`Squarefree` `CommMonoid.toMonoid`	—	`isUnit_or_isUnit` `mul_assoc` `isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid`

IsRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`isUnit_iff_dvd_one` `mul_dvd_mul_iff_right` `mul_ne_zero_iff` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `mul_assoc` `one_mul` `pow_two` `mul_left_comm`

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_squarefree_mul` 📖	mathematical	`Squarefree` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsRelPrime` `CommMonoid.toMonoid`	—	`mul_dvd_mul`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`Squarefree` `CommMonoid.toMonoid`	—	`isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid` `isUnit_of_dvd_unit`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree` 📖	mathematical	`Prime`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Irreducible.squarefree` `irreducible`

Squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_squarefree_of_mul_dvd_mul_left` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`dvd_of_squarefree_of_mul_dvd_mul_right` `mul_comm`
`dvd_of_squarefree_of_mul_dvd_mul_right` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `exists_dvd_and_dvd_of_dvd_mul` `squarefree_of_dvd` `isRadical` `sq` `dvd_trans` `mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `ne_zero` `mul_assoc` `mul_comm`
`dvd_pow_iff_dvd` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid`	—	`isRadical` `Dvd.dvd.pow`
`eq_zero_or_one_of_pow_of_not_isUnit` 📖	—	`Squarefree` `Monoid.toPow` `IsUnit`	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `sq` `pow_dvd_pow` `squarefree_of_dvd` `refl` `instReflDvd_mathlib`
`gcd_left` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `GCDMonoid.gcd`	—	`squarefree_of_dvd` `GCDMonoid.gcd_dvd_left`
`gcd_right` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `GCDMonoid.gcd`	—	`squarefree_of_dvd` `GCDMonoid.gcd_dvd_right`
`isRadical` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid`	—	`isRadical_iff_pow_one_lt` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `exists_dvd_and_dvd_of_dvd_mul` `sq` `IsRelPrime.mul_dvd` `IsRelPrime.of_squarefree_mul`
`ne_zero` 📖	—	`Squarefree` `MonoidWithZero.toMonoid`	—	—	`not_squarefree_zero`
`of_mul_left` 📖	mathematical	`Squarefree` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Squarefree`	—	`dvd_mul_of_dvd_left`
`of_mul_right` 📖	mathematical	`Squarefree` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Squarefree` `CommMonoid.toMonoid`	—	`dvd_mul_of_dvd_right`
`pow_dvd_of_pow_dvd` 📖	mathematical	`Squarefree` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toPow`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toPow`	—	`IsUnit.dvd` `IsUnit.pow` `eq_zero_or_one_of_pow_of_not_isUnit` `squarefree_of_dvd` `pow_zero` `pow_one`
`pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toPow` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid`	—	`pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right` `mul_comm`
`pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right` 📖	mathematical	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toPow` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid`	—	`Prime.not_unit` `mul_dvd_mul_left` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `Prime.ne_zero` `mul_assoc` `pow_succ'` `Prime.pow_dvd_of_dvd_mul_left` `Dvd.dvd.trans` `pow_dvd_pow`
`squarefree_of_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `Squarefree`	`Squarefree`	—	`Dvd.dvd.trans`

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`squarefree_iff_nodup_normalizedFactors` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.Nodup` `normalizedFactors`	—	`squarefree_iff_emultiplicity_le_one` `Multiset.nodup_iff_count_le_one` `irreducible_of_normalized_factor` `normalize_normalized_factor` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `emultiplicity_eq_count_normalizedFactors` `Irreducible.not_isUnit` `Multiset.count_eq_zero_of_notMem` `Nat.instCanonicallyOrderedAdd` `eq_or_ne` `emultiplicity_zero_eq_zero_of_ne_zero` `WfDvdMonoid.exists_irreducible_factor` `toIsWellFounded` `le_trans` `emultiplicity_le_emultiplicity_of_dvd_left`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_squarefree_dvd_pow_of_ne_zero` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toPow`	—	`WfDvdMonoid.induction_on_irreducible` `UniqueFactorizationMonoid.toIsWellFounded` `squarefree_one` `one_dvd` `IsUnit.dvd` `Irreducible.squarefree` `dvd_mul_right` `pow_one` `isUnit_of_dvd_one` `pow_zero` `dvd_mul_of_dvd_right` `mul_dvd_mul` `pow_succ` `mul_comm` `squarefree_mul_iff` `UniqueFactorizationMonoid.toIsCancelMulZero` `instDecompositionMonoidOfNonemptyGCDMonoid` `instNonemptyGCDMonoidOfNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid` `Irreducible.isRelPrime_iff_not_dvd` `mul_dvd_mul_left` `dvd_pow_self` `LT.lt.ne'` `mul_pow`
`irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulZeroClass.toZero` `Irreducible` `MonoidWithZero.toMonoid` `Squarefree`	—	`eq_or_ne` `squarefree_iff_no_irreducibles` `Irreducible.not_isUnit`
`isRadical_iff_squarefree_of_ne_zero` 📖	mathematical	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid` `Squarefree`	—	`IsRadical.squarefree` `Squarefree.isRadical`
`isRadical_iff_squarefree_or_zero` 📖	mathematical	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toPow` `MonoidWithZero.toMonoid` `Squarefree` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`em` `IsRadical.squarefree` `Squarefree.isRadical` `zero_isRadical_iff` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero`
`not_squarefree_zero` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Squarefree.eq_1` `MulZeroClass.mul_zero` `NeZero.one`
`squarefree_iff_emultiplicity_le_one` 📖	mathematical	—	`Squarefree` `CommMonoid.toMonoid` `ENat` `instLEENat` `emultiplicity` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `IsUnit`	—	`sq` `pow_dvd_iff_le_emultiplicity` `not_le` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `one_add_one_eq_two` `Order.add_one_le_iff_of_not_isMax`
`squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree`
`squarefree_iff_irreducible_sq_not_dvd_of_ne_zero` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree`
`squarefree_iff_no_irreducibles` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Irreducible.not_isUnit` `by_contra` `ne_zero_of_dvd_ne_zero` `dvd_mul_left` `WfDvdMonoid.exists_irreducible_factor` `Dvd.dvd.trans` `mul_dvd_mul`
`squarefree_mul_iff` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsRelPrime`	—	`IsRelPrime.of_squarefree_mul` `Squarefree.of_mul_left` `Squarefree.of_mul_right` `Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left` `Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right`
`squarefree_one` 📖	mathematical	—	`Squarefree` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsUnit.squarefree` `isUnit_one`

---

← Back to Index