Radical

📁 Source: Mathlib/RingTheory/Radical.lean

Statistics

Metric	Count
Definitions `divRadical`, `primeFactors`, `radical`	3
Theorems `primeFactors_eq`, `divRadical_dvd_self`, `divRadical_isUnit`, `divRadical_mul`, `divRadical_mul_radical`, `divRadical_ne_zero`, `eq_divRadical`, `radical_mul_divRadical`, `divRadical`, `dvd_radical`, `one_lt_radical_iff`, `radical_le_one_iff`, `radical_le_self_iff`, `radical_pos`, `two_le_radical_iff`, `radical_neg`, `radical_neg_one`, `disjoint_primeFactors`, `dvd_radical_iff`, `dvd_radical_iff_of_irreducible`, `isRadical_radical`, `mem_primeFactors`, `normalizedFactors_nodup`, `pairwise_primeFactors_isRelPrime`, `primeFactors_eq_empty_iff`, `primeFactors_eq_natPrimeFactors`, `primeFactors_mul_eq_disjUnion`, `primeFactors_mul_eq_union`, `primeFactors_of_isUnit`, `primeFactors_one`, `primeFactors_pow`, `primeFactors_pow'`, `primeFactors_radical`, `primeFactors_val_eq_normalizedFactors`, `primeFactors_zero`, `radical_associated`, `radical_dvd_iff_primeFactors_subset`, `radical_dvd_radical`, `radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors`, `radical_dvd_radical_iff_primeFactors_subset_primeFactors`, `radical_dvd_self`, `radical_eq_iff_primeFactors_eq`, `radical_eq_of_associated`, `radical_eq_of_primeFactors_eq`, `radical_eq_one_iff`, `radical_mul`, `radical_mul_dvd`, `radical_mul_of_isUnit_left`, `radical_mul_of_isUnit_right`, `radical_ne_zero`, `radical_of_isUnit`, `radical_of_prime`, `radical_one`, `radical_pow`, `radical_pow_of_prime`, `radical_prod`, `radical_prod_dvd`, `radical_radical`, `radical_zero`, `squarefree_radical`	60
Total	63

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primeFactors_eq` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`UniqueFactorizationMonoid.primeFactors`	—	`normalizedFactors_eq`

EuclideanDomain

Definitions

Name	Category	Theorems
`divRadical` 📖	CompOp	10 math math: `divRadical_dvd_self`, `divRadical_mul`, `radical_mul_divRadical`, `divRadical_dvd_derivative`, `eq_divRadical`, `IsCoprime.divRadical`, `divRadical_dvd_wronskian_right`, `divRadical_isUnit`, `divRadical_dvd_wronskian_left`, `divRadical_mul_radical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divRadical_dvd_self` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `toCommRing` `divRadical`	—	`divRadical_mul_radical`
`divRadical_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toCommRing`	`divRadical`	—	`divRadical.eq_1` `UniqueFactorizationMonoid.radical_of_isUnit` `div_one`
`divRadical_mul` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring` `toCommRing`	`divRadical` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`eq_divRadical` `UniqueFactorizationMonoid.radical_mul` `IsCoprime.isRelPrime` `mul_mul_mul_comm` `radical_mul_divRadical`
`divRadical_mul_radical` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toCommRing` `divRadical` `UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	—	`mul_comm` `radical_mul_divRadical`
`divRadical_ne_zero` 📖	—	—	—	—	`right_ne_zero_of_mul` `radical_mul_divRadical`
`eq_divRadical` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toCommRing` `UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	`divRadical`	—	`eq_div_of_mul_eq_left` `UniqueFactorizationMonoid.radical_ne_zero` `toNontrivial` `mul_comm`
`radical_mul_divRadical` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toCommRing` `UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `divRadical`	—	`divRadical.eq_1` `mul_div_assoc` `UniqueFactorizationMonoid.radical_dvd_self` `mul_div_cancel_left₀` `toMulDivCancelClass` `UniqueFactorizationMonoid.radical_ne_zero` `toNontrivial`

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divRadical` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing`	`EuclideanDomain.divRadical`	—	`of_mul_right_right` `of_mul_left_right` `EuclideanDomain.radical_mul_divRadical`

IsRadical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_radical` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`UniqueFactorizationMonoid.radical`	—	`Associated.dvd'` `UniqueFactorizationMonoid.radical_associated`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`two_le_radical_iff`
`radical_le_one_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `Iff.not` `one_lt_radical_iff`
`radical_le_self_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.radical_zero` `instCanonicallyOrderedAdd` `UniqueFactorizationMonoid.radical_dvd_self`
`radical_pos` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`pos_of_ne_zero` `instCanonicallyOrderedAdd` `Unique.instSubsingleton` `instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.radical_ne_zero` `instNontrivial`
`two_le_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.radical_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `instCharZero` `instAtLeastTwoHAddOfNat` `instCanonicallyOrderedAdd` `UniqueFactorizationMonoid.radical_one` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `exists_prime_and_dvd` `Prime.two_le` `UniqueFactorizationMonoid.radical_ne_zero` `instNontrivial` `UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible` `Prime.irreducible` `instIsCancelMulZero` `Prime.prime`

UniqueFactorizationDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`radical_neg` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`UniqueFactorizationMonoid.radical_eq_of_associated` `Associated.neg_left` `Associated.rfl`
`radical_neg_one` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`radical_neg` `UniqueFactorizationMonoid.radical_one`

UniqueFactorizationMonoid

Definitions

Name	Category	Theorems
`primeFactors` 📖	CompOp	18 math math: `primeFactors_zero`, `primeFactors_pow'`, `primeFactors_one`, `primeFactors_mul_eq_union`, `primeFactors_mul_eq_disjUnion`, `primeFactors_pow`, `radical_dvd_radical_iff_primeFactors_subset_primeFactors`, `mem_primeFactors`, `primeFactors_radical`, `pairwise_primeFactors_isRelPrime`, `primeFactors_eq_natPrimeFactors`, `primeFactors_eq_empty_iff`, `radical_eq_iff_primeFactors_eq`, `primeFactors_val_eq_normalizedFactors`, `radical_dvd_iff_primeFactors_subset`, `disjoint_primeFactors`, `primeFactors_of_isUnit`, `Associated.primeFactors_eq`
`radical` 📖	CompOp	41 math math: `dvd_radical_iff`, `squarefree_radical`, `radical_prod`, `Polynomial.abc`, `isRadical_radical`, `Nat.two_le_radical_iff`, `EuclideanDomain.radical_mul_divRadical`, `Nat.radical_pos`, `radical_eq_of_associated`, `radical_of_prime`, `radical_associated`, `radical_radical`, `radical_dvd_radical_iff_primeFactors_subset_primeFactors`, `Nat.radical_le_self_iff`, `radical_one`, `radical_mul_of_isUnit_right`, `natDegree_radical_le`, `dvd_radical_iff_of_irreducible`, `radical_prod_dvd`, `radical_zero`, `radical_pow`, `radical_dvd_self`, `primeFactors_radical`, `radical_of_isUnit`, `IsRadical.dvd_radical`, `UniqueFactorizationDomain.radical_neg_one`, `radical_eq_iff_primeFactors_eq`, `radical_dvd_iff_primeFactors_subset`, `Nat.one_lt_radical_iff`, `radical_mul_dvd`, `radical_mul_of_isUnit_left`, `radical_pow_of_prime`, `radical_eq_of_primeFactors_eq`, `radical_dvd_radical`, `Nat.radical_le_one_iff`, `EuclideanDomain.divRadical_mul_radical`, `radical_eq_one_iff`, `radical_mul`, `radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors`, `UniqueFactorizationDomain.radical_neg`, `degree_radical_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_primeFactors` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `primeFactors`	—	`Multiset.disjoint_toFinset` `disjoint_normalizedFactors`
`dvd_radical_iff` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`radical`	—	`Dvd.dvd.trans` `radical_dvd_self` `eq_or_ne` `IsRadical.dvd_radical` `radical_dvd_radical`
`dvd_radical_iff_of_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `radical`	—	`Dvd.dvd.trans` `radical_dvd_self` `exists_mem_normalizedFactors_of_dvd` `Associated.dvd` `Finset.dvd_prod_of_mem`
`isRadical_radical` 📖	mathematical	—	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `radical`	—	`radical.eq_1` `Finset.prod_dvd_of_isRelPrime` `instDecompositionMonoid` `pairwise_primeFactors_isRelPrime` `dvd_radical_iff_of_irreducible` `irreducible_of_normalized_factor` `normalizedFactors_zero` `dvd_of_mem_normalizedFactors` `Prime.isRadical` `prime_of_normalized_factor` `Dvd.dvd.trans`
`mem_primeFactors` 📖	mathematical	—	`Finset` `Finset.instMembership` `primeFactors` `Multiset` `Multiset.instMembership` `normalizedFactors`	—	—
`normalizedFactors_nodup` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`Multiset.Nodup` `normalizedFactors`	—	`eq_or_ne` `normalizedFactors_zero` `squarefree_iff_nodup_normalizedFactors` `isRadical_iff_squarefree_of_ne_zero` `toIsCancelMulZero` `instDecompositionMonoid`
`pairwise_primeFactors_isRelPrime` 📖	mathematical	—	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `primeFactors` `IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`eq_or_ne` `primeFactors_zero` `Finset.coe_empty` `Irreducible.isRelPrime_iff_not_dvd` `mem_normalizedFactors_iff'` `Mathlib.Tactic.Contrapose.contrapose₄` `Irreducible.associated_of_dvd` `Associated.eq_of_normalized` `toIsCancelMulZero`
`primeFactors_eq_empty_iff` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instEmptyCollection` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`primeFactors.eq_1` `Multiset.toFinset_eq_empty` `normalizedFactors_eq_zero_iff`
`primeFactors_eq_natPrimeFactors` 📖	mathematical	—	`primeFactors` `Nat.instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Nat.unique_units` `Nat.instUniqueFactorizationMonoid` `Nat.primeFactors`	—	`Unique.instSubsingleton` `Nat.instUniqueFactorizationMonoid` `primeFactors.eq_1` `Nat.factors_eq` `Nat.primeFactors.eq_1` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `List.toFinset_coe`
`primeFactors_mul_eq_disjUnion` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`primeFactors` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Finset.disjUnion` `disjoint_primeFactors`	—	`disjoint_primeFactors` `eq_or_ne` `primeFactors.congr_simp` `MulZeroClass.zero_mul` `primeFactors_zero` `primeFactors_of_isUnit` `isRelPrime_zero_left` `Finset.disjUnion.congr_simp` `Finset.empty_disjUnion` `MulZeroClass.mul_zero` `isRelPrime_zero_right` `Finset.disjUnion_empty` `Finset.disjUnion_eq_union` `primeFactors_mul_eq_union`
`primeFactors_mul_eq_union` 📖	mathematical	—	`primeFactors` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finset` `Finset.instUnion`	—	`Finset.ext` `normalizedFactors_mul`
`primeFactors_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`primeFactors` `Finset` `Finset.instEmptyCollection`	—	`primeFactors.eq_1` `normalizedFactors_of_isUnit` `Multiset.toFinset_zero`
`primeFactors_one` 📖	mathematical	—	`primeFactors` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finset` `Finset.instEmptyCollection`	—	`normalizedFactors_one`
`primeFactors_pow` 📖	mathematical	—	`primeFactors` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`normalizedFactors_pow` `Multiset.toFinset_nsmul`
`primeFactors_pow'` 📖	mathematical	—	`primeFactors` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`primeFactors_pow`
`primeFactors_radical` 📖	mathematical	—	`primeFactors` `radical`	—	`eq_or_ne` `normalizedFactors.congr_simp` `radical_zero` `normalizedFactors_one` `normalizedFactors_zero` `Finset.ext`
`primeFactors_val_eq_normalizedFactors` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`Finset.val` `primeFactors` `normalizedFactors`	—	`primeFactors.eq_1` `Multiset.toFinset_val` `Multiset.dedup_eq_self` `normalizedFactors_nodup`
`primeFactors_zero` 📖	mathematical	—	`primeFactors` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Finset` `Finset.instEmptyCollection`	—	`normalizedFactors_zero`
`radical_associated` 📖	mathematical	`IsRadical` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`Associated` `radical`	—	`radical.eq_1` `Finset.prod_val` `primeFactors_val_eq_normalizedFactors` `prod_normalizedFactors`
`radical_dvd_iff_primeFactors_subset` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical` `Finset` `Finset.instHasSubset` `primeFactors`	—	`dvd_radical_iff` `isRadical_radical` `radical_dvd_radical_iff_primeFactors_subset_primeFactors`
`radical_dvd_radical` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	`radical`	—	`eq_or_ne` `radical_zero` `radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors` `Multiset.subset_of_le` `dvd_iff_normalizedFactors_le_normalizedFactors`
`radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical` `Multiset` `Multiset.instHasSubset` `normalizedFactors`	—	`eq_or_ne` `radical_zero` `normalizedFactors_zero` `dvd_iff_normalizedFactors_le_normalizedFactors` `radical_ne_zero` `Multiset.le_iff_subset` `normalizedFactors_nodup` `isRadical_radical` `primeFactors_radical`
`radical_dvd_radical_iff_primeFactors_subset_primeFactors` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical` `Finset` `Finset.instHasSubset` `primeFactors`	—	`radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors` `primeFactors.eq_1` `Multiset.toFinset_subset`
`radical_dvd_self` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical`	—	`dvd_zero` `radical.eq_1` `Finset.prod_val` `Associated.dvd_iff_dvd_right` `prod_normalizedFactors` `Multiset.prod_dvd_prod_of_le` `primeFactors.eq_1` `Multiset.toFinset_val` `Multiset.dedup_le`
`radical_eq_iff_primeFactors_eq` 📖	mathematical	—	`radical` `primeFactors`	—	`primeFactors_radical` `Finset.prod_congr`
`radical_eq_of_associated` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical`	—	`radical.eq_1` `Associated.primeFactors_eq`
`radical_eq_of_primeFactors_eq` 📖	mathematical	`primeFactors`	`radical`	—	`radical_eq_iff_primeFactors_eq`
`radical_eq_one_iff` 📖	mathematical	—	`radical` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `IsUnit` `MonoidWithZero.toMonoid`	—	`primeFactors_radical` `primeFactors_one` `primeFactors_eq_empty_iff` `radical.congr_simp` `radical_zero` `radical_of_isUnit`
`radical_mul` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`disjoint_primeFactors` `primeFactors_mul_eq_disjUnion` `Finset.prod_disjUnion`
`radical_mul_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`eq_or_ne` `radical.congr_simp` `MulZeroClass.zero_mul` `radical_zero` `one_mul` `MulZeroClass.mul_zero` `mul_one` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `primeFactors_mul_eq_union` `primeFactors_radical` `Finset.instReflSubset`
`radical_mul_of_isUnit_left` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`radical_eq_of_associated` `associated_unit_mul_left`
`radical_mul_of_isUnit_right` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`radical_eq_of_associated` `associated_mul_unit_left`
`radical_ne_zero` 📖	—	—	—	—	`radical.eq_1` `Finset.prod_val` `Multiset.prod_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `primeFactors.eq_1` `zero_notMem_normalizedFactors`
`radical_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass`	—	`radical_eq_of_associated` `associated_one_iff_isUnit` `radical_one`
`radical_of_prime` 📖	mathematical	`Prime`	`radical` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize`	—	`radical.eq_1` `primeFactors.eq_1` `normalizedFactors_irreducible` `Prime.irreducible` `toIsCancelMulZero` `Finset.prod_congr` `Multiset.toFinset_singleton` `Finset.prod_singleton`
`radical_one` 📖	mathematical	—	`radical` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`Finset.prod_congr` `primeFactors_one`
`radical_pow` 📖	mathematical	—	`radical` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Finset.prod_congr` `primeFactors_pow`
`radical_pow_of_prime` 📖	mathematical	`Prime`	`radical` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize`	—	`radical_pow` `radical_of_prime`
`radical_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`radical` `Finset.prod` `CommMonoidWithZero.toCommMonoid`	—	`Finset.cons_induction` `radical_one` `radical.congr_simp` `Finset.prod_cons` `radical_mul` `IsRelPrime.prod_right` `instDecompositionMonoid` `Set.pairwise_insert_of_symmetric_of_notMem` `Symmetric.comap` `symmetric_isRelPrime` `Finset.coe_cons`
`radical_prod_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `radical` `Finset.prod` `CommMonoidWithZero.toCommMonoid`	—	`Finset.cons_induction` `radical_one` `radical.congr_simp` `Finset.prod_cons` `Dvd.dvd.trans` `radical_mul_dvd` `mul_dvd_mul_left`
`radical_radical` 📖	mathematical	—	`radical`	—	`radical_eq_iff_primeFactors_eq` `primeFactors_radical`
`radical_zero` 📖	mathematical	—	`radical` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`Finset.prod_congr` `primeFactors_zero`
`squarefree_radical` 📖	mathematical	—	`Squarefree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `radical`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `IsRadical.squarefree` `toIsCancelMulZero` `isRadical_radical`

---

← Back to Index