Content

📁 Source: Mathlib/RingTheory/Polynomial/Content.lean

Statistics

Metric	Count
Definitions `IsPrimitive`, `content`, `normalizedGcdMonoid`, `primPart`	4
Theorems `isPrimitive`, `C_content_dvd`, `content_eq_one`, `dvd_primPart_iff_dvd`, `mul`, `ne_zero`, `primPart_eq`, `isPrimitive`, `aeval_primPart_eq_zero`, `content_C`, `content_C_mul`, `content_X`, `content_X_mul`, `content_X_pow`, `content_dvd_coeff`, `content_eq_gcd_leadingCoeff_content_eraseLead`, `content_eq_gcd_range_of_lt`, `content_eq_gcd_range_succ`, `content_eq_zero_iff`, `content_monomial`, `content_mul`, `content_mul_aux`, `content_one`, `content_primPart`, `content_zero`, `degree_gcd_le_left`, `degree_gcd_le_right`, `dvd_content_iff_C_dvd`, `dvd_iff_content_dvd_content_and_primPart_dvd_primPart`, `eq_C_content_mul_primPart`, `eval₂_primPart_eq_zero`, `exists_primitive_lcm_of_isPrimitive`, `gcd_content_eq_of_dvd_sub`, `isPrimitive_iff_content_eq_one`, `isPrimitive_iff_isUnit_of_C_dvd`, `isPrimitive_iff_ne_zero`, `isPrimitive_of_dvd`, `isPrimitive_one`, `isPrimitive_primPart`, `isUnit_primPart_C`, `natDegree_primPart`, `normUnit_content`, `normalize_content`, `primPart_dvd`, `primPart_mul`, `primPart_ne_zero`, `primPart_zero`	47
Total	51

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimitive` 📖	mathematical	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.IsPrimitive`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `Polynomial.isUnit_iff` `Polynomial.natDegree_C_mul` `Polynomial.natDegree_C` `Polynomial.coeff_C_zero` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `isUnit_or_isUnit`

Polynomial

Definitions

Name	Category	Theorems
`IsPrimitive` 📖	MathDef	12 math math: `isPrimitive_iff_isUnit_of_C_dvd`, `Irreducible.isPrimitive`, `isPrimitive_iff_content_eq_one`, `isPrimitive_iff_contentIdeal_eq_top`, `isPrimitive_iff_ne_zero`, `isPrimitive_of_contentIdeal_eq_top`, `cyclotomic.isPrimitive`, `isPrimitive_primPart`, `isPrimitive_one`, `Monic.isPrimitive`, `isPrimitive_iff_forall_gaussNorm_eq_one`, `Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top`
`content` 📖	CompOp	27 math math: `dvd_iff_content_dvd_content_and_primPart_dvd_primPart`, `content_eq_zero_iff`, `content_zero`, `content_eq_gcd_range_of_lt`, `normUnit_content`, `isPrimitive_iff_content_eq_one`, `IsPrimitive.content_eq_one`, `content_X_mul`, `gcd_content_eq_of_dvd_sub`, `content_C_mul`, `eq_C_content_mul_primPart`, `normalize_content`, `content_mul_aux`, `Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal`, `content_one`, `dvd_content_iff_C_dvd`, `content_X`, `content_dvd_coeff`, `content_primPart`, `content_mul`, `contentIdeal_le_span_content`, `content_C`, `content_eq_gcd_leadingCoeff_content_eraseLead`, `content_eq_gcd_range_succ`, `content_X_pow`, `C_content_dvd`, `content_monomial`
`normalizedGcdMonoid` 📖	CompOp	6 math math: `RatFunc.num_div`, `degree_gcd_le_left`, `RatFunc.numDenom_div`, `RatFunc.denom_div`, `RatFunc.num_div_dvd'`, `degree_gcd_le_right`
`primPart` 📖	CompOp	13 math math: `primPart_zero`, `aeval_primPart_eq_zero`, `dvd_iff_content_dvd_content_and_primPart_dvd_primPart`, `eq_C_content_mul_primPart`, `natDegree_primPart`, `primPart_dvd`, `isPrimitive_primPart`, `IsPrimitive.dvd_primPart_iff_dvd`, `isUnit_primPart_C`, `IsPrimitive.primPart_eq`, `content_primPart`, `eval₂_primPart_eq_zero`, `primPart_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_content_dvd` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `content`	—	`dvd_content_iff_C_dvd` `dvd_rfl`
`aeval_primPart_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `Ring.toSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`primPart`	—	`eq_zero_of_ne_zero_of_mul_left_eq_zero` `IsDomain.to_noZeroDivisors` `Module.nontrivial` `IsDomain.toNontrivial` `GCDMonoid.toIsCancelMulZero` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `content_eq_zero_iff` `aeval_C` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `eq_C_content_mul_primPart`
`content_C` 📖	mathematical	—	`content` `DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`content.eq_1` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `support_monomial` `Finset.gcd_singleton` `coeff_C_zero`
`content_C_mul` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `content_zero` `MonoidWithZeroHom.monoidWithZeroHomClass` `content.eq_1` `Finset.gcd_mul_left` `Finset.ext` `coeff_C_mul` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero`
`content_X` 📖	mathematical	—	`content` `X` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`mul_one` `content_X_mul` `content_one`
`content_X_mul` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul` `X`	—	`content.eq_1` `Finset.gcd_def` `Nat.succ_injective` `Finset.ext` `mul_coeff_zero` `coeff_X_zero` `MulZeroClass.zero_mul` `mul_comm` `coeff_mul_X` `Multiset.map_congr` `Multiset.map_map`
`content_X_pow` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`pow_zero` `content_one` `pow_succ'` `content_X_mul`
`content_dvd_coeff` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `content` `coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Finset.gcd_dvd` `mem_support_iff` `dvd_zero`
`content_eq_gcd_leadingCoeff_content_eraseLead` 📖	mathematical	—	`content` `GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NormalizedGCDMonoid.toGCDMonoid` `leadingCoeff` `CommSemiring.toSemiring` `eraseLead`	—	`content_zero` `eraseLead_zero` `gcd_same` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `content.eq_1` `Finset.insert_erase` `mem_support_iff` `leadingCoeff.eq_1` `leadingCoeff_eq_zero` `Finset.gcd_insert` `eraseLead_support` `Finset.gcd_congr` `eraseLead_coeff` `Finset.mem_erase`
`content_eq_gcd_range_of_lt` 📖	mathematical	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`content` `Finset.gcd` `CommSemiring.toCommMonoidWithZero` `Finset.range` `coeff`	—	`dvd_antisymm_of_normalize_eq` `GCDMonoid.toIsCancelMulZero` `normalize_content` `Finset.normalize_gcd` `Finset.dvd_gcd_iff` `content_dvd_coeff` `Finset.gcd_mono` `Mathlib.Tactic.Contrapose.contrapose₂` `coeff_eq_zero_of_natDegree_lt` `lt_of_lt_of_le`
`content_eq_gcd_range_succ` 📖	mathematical	—	`content` `Finset.gcd` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Finset.range` `natDegree` `CommSemiring.toSemiring` `coeff`	—	`content_eq_gcd_range_of_lt`
`content_eq_zero_iff` 📖	mathematical	—	`content` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instZero`	—	`content.eq_1` `Finset.gcd_eq_zero_iff` `ext` `coeff_zero` `mem_support_iff`
`content_monomial` 📖	mathematical	—	`content` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid`	—	`C_mul_X_pow_eq_monomial` `content_C_mul` `content_X_pow` `mul_one`
`content_mul` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `mul_eq_zero` `instNoZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero` `degree_eq_bot` `Nat.WithBot.lt_zero_iff` `Nat.cast_zero` `MulZeroClass.zero_mul` `content_zero` `MulZeroClass.mul_zero` `natDegree_mul` `degree_eq_natDegree` `mul_ne_zero` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `eq_C_content_mul_primPart` `normalize_content` `normalize_eq_one` `isUnit_iff_dvd_one` `content_eq_gcd_leadingCoeff_content_eraseLead` `leadingCoeff_mul` `gcd_comm` `Dvd.dvd.trans` `gcd_mul_dvd_mul_gcd` `content_mul_aux` `mul_comm` `primPart_ne_zero` `Nat.cast_add` `natDegree_primPart` `degree_mul` `WithBot.add_lt_add_iff_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `degree_erase_lt` `content_primPart` `mul_one` `one_mul` `WithBot.add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `dvd_refl` `mul_assoc` `content_C_mul` `lt_of_le_of_lt` `degree_le_natDegree` `WithBot.coe_lt_coe`
`content_mul_aux` 📖	mathematical	—	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NormalizedGCDMonoid.toGCDMonoid` `content` `eraseLead` `CommSemiring.toSemiring` `Polynomial` `instMul` `leadingCoeff`	—	`gcd_comm` `gcd_content_eq_of_dvd_sub` `self_sub_C_mul_X_pow` `sub_mul` `sub_sub` `add_comm` `sub_add` `sub_sub_cancel` `leadingCoeff_mul` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `dvd_sub` `Dvd.intro`
`content_one` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`C_1` `content_C` `normalize_one`
`content_primPart` 📖	mathematical	—	`content` `primPart` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`IsPrimitive.content_eq_one` `isPrimitive_primPart`
`content_zero` 📖	mathematical	—	`content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`C_0` `content_C` `normalize_zero`
`degree_gcd_le_left` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GCDMonoid.gcd` `Polynomial` `CommSemiring.toCommMonoidWithZero` `commSemiring` `NormalizedGCDMonoid.toGCDMonoid` `normalizedGcdMonoid`	—	`natDegree_le_iff_degree_le` `natDegree_le_of_dvd` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero` `GCDMonoid.gcd_dvd_left` `degree_eq_natDegree`
`degree_gcd_le_right` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GCDMonoid.gcd` `Polynomial` `CommSemiring.toCommMonoidWithZero` `commSemiring` `NormalizedGCDMonoid.toGCDMonoid` `normalizedGcdMonoid`	—	`gcd_comm` `degree_gcd_le_left`
`dvd_content_iff_C_dvd` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `content` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`C_dvd_iff_dvd_coeff` `Dvd.dvd.trans` `content_dvd_coeff` `content.eq_1` `Finset.dvd_gcd_iff`
`dvd_iff_content_dvd_content_and_primPart_dvd_primPart` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `content` `primPart`	—	`content_mul` `IsPrimitive.dvd_primPart_iff_dvd` `isPrimitive_primPart` `dvd_mul_right` `dvd_mul_of_dvd_left` `primPart_dvd` `eq_C_content_mul_primPart` `mul_dvd_mul` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`eq_C_content_mul_primPart` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `content` `primPart`	—	`content_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `C_content_dvd` `primPart.eq_1`
`eval₂_primPart_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `eval₂` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`primPart`	—	`eq_zero_of_ne_zero_of_mul_left_eq_zero` `IsDomain.to_noZeroDivisors` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `content_eq_zero_iff` `eval₂_C` `eval₂_mul` `eq_C_content_mul_primPart`
`exists_primitive_lcm_of_isPrimitive` 📖	mathematical	`IsPrimitive` `CommRing.toCommSemiring`	`Polynomial` `CommSemiring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing`	—	`IsPrimitive.mul` `dvd_mul_right` `dvd_mul_left` `Nat.find_spec` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Contrapose.contrapose₄` `Nat.find_min'` `natDegree_primPart` `isPrimitive_primPart` `IsPrimitive.dvd_primPart_iff_dvd` `dvd_content_iff_C_dvd` `eq_C_of_natDegree_le_zero` `le_trans` `IsUnit.dvd` `normalize_eq_one` `content_C` `isPrimitive_iff_content_eq_one` `natDegree_cancelLeads_lt_of_natDegree_le_natDegree` `Nat.find_min` `dvd_cancelLeads_of_dvd_of_dvd` `dvd_add` `Distrib.leftDistribClass` `mul_one` `pow_zero` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `cancelLeads.eq_1` `Dvd.intro_left` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `IsPrimitive.ne_zero` `isUnit_primPart_C` `Dvd.dvd.trans` `mul_ne_zero` `instNoZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero` `C_eq_zero` `leadingCoeff_eq_zero` `sub_add_cancel` `Associated.dvd` `Associated.symm` `primPart_mul` `mul_comm`
`gcd_content_eq_of_dvd_sub` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instSub` `CommRing.toRing`	`GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero` `NormalizedGCDMonoid.toGCDMonoid` `content`	—	`content_eq_gcd_range_of_lt` `lt_of_le_of_lt` `le_max_left` `le_max_right` `Finset.gcd_eq_of_dvd_sub` `coeff_sub` `coeff_C_mul`
`isPrimitive_iff_content_eq_one` 📖	mathematical	—	`IsPrimitive` `CommRing.toCommSemiring` `content` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`normalize_content` `normalize_eq_one` `IsPrimitive.eq_1` `dvd_refl` `isUnit_of_dvd_unit`
`isPrimitive_iff_isUnit_of_C_dvd` 📖	mathematical	—	`IsPrimitive` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	—
`isPrimitive_iff_ne_zero` 📖	mathematical	—	`IsPrimitive` `Semifield.toCommSemiring` `Field.toSemifield`	—	`IsPrimitive.ne_zero` `EuclideanDomain.toNontrivial` `ne_zero_of_dvd_ne_zero` `C_0`
`isPrimitive_of_dvd` 📖	—	`IsPrimitive` `Polynomial` `CommSemiring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	—	—	`isPrimitive_iff_isUnit_of_C_dvd` `dvd_trans`
`isPrimitive_one` 📖	mathematical	—	`IsPrimitive` `Polynomial` `CommSemiring.toSemiring` `instOne`	—	`isUnit_C` `isUnit_of_dvd_one`
`isPrimitive_primPart` 📖	mathematical	—	`IsPrimitive` `CommRing.toCommSemiring` `primPart`	—	`primPart_zero` `isPrimitive_iff_content_eq_one` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `content_eq_zero_iff` `eq_C_content_mul_primPart` `mul_one` `content_C_mul` `normalize_content`
`isUnit_primPart_C` 📖	mathematical	—	`IsUnit` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `primPart` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `primPart_zero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Units.inv_mul` `C_1` `Units.mul_inv` `mul_left_cancel₀` `instIsLeftCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `C_eq_zero` `normalize_eq_zero` `content_C` `eq_C_content_mul_primPart` `mul_assoc` `mul_one`
`natDegree_primPart` 📖	mathematical	—	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `primPart`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `natDegree_of_subsingleton` `content_eq_zero_iff` `C_eq_zero` `primPart_zero` `natDegree_one` `eq_C_content_mul_primPart` `natDegree_mul` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `GCDMonoid.toIsCancelMulZero` `primPart_ne_zero` `natDegree_C` `zero_add`
`normUnit_content` 📖	mathematical	—	`NormalizationMonoid.normUnit` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `NormalizedGCDMonoid.toNormalizationMonoid` `content` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Units.instOne`	—	`NormalizationMonoid.normUnit_zero` `Units.ext` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `normalize_apply` `normalize_content` `Units.val_one` `mul_one`
`normalize_content` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `NormalizedGCDMonoid.toNormalizationMonoid` `content`	—	`Finset.normalize_gcd`
`primPart_dvd` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `primPart`	—	`Dvd.intro_left` `eq_C_content_mul_primPart`
`primPart_mul` 📖	mathematical	—	`primPart` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul`	—	`mul_left_cancel₀` `instIsLeftCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `GCDMonoid.toIsCancelMulZero` `C_eq_zero` `content_eq_zero_iff` `eq_C_content_mul_primPart` `content_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`primPart_ne_zero` 📖	—	—	—	—	`IsPrimitive.ne_zero` `isPrimitive_primPart`
`primPart_zero` 📖	mathematical	—	`primPart` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instZero` `instOne`	—	`C_content_dvd`

Polynomial.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`content_eq_one` 📖	mathematical	`Polynomial.IsPrimitive` `CommRing.toCommSemiring`	`Polynomial.content` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Polynomial.isPrimitive_iff_content_eq_one`
`dvd_primPart_iff_dvd` 📖	mathematical	`Polynomial.IsPrimitive` `CommRing.toCommSemiring`	`Polynomial` `CommSemiring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Polynomial.primPart`	—	`Dvd.dvd.trans` `Dvd.intro_left` `Polynomial.eq_C_content_mul_primPart` `Dvd.intro` `Polynomial.primPart_mul` `primPart_eq`
`mul` 📖	mathematical	`Polynomial.IsPrimitive` `CommRing.toCommSemiring`	`Polynomial` `CommSemiring.toSemiring` `Polynomial.instMul`	—	`Polynomial.isPrimitive_iff_content_eq_one` `Polynomial.content_mul` `content_eq_one` `mul_one`
`ne_zero` 📖	—	`Polynomial.IsPrimitive`	—	—	`IsUnit.ne_zero` `dvd_zero`
`primPart_eq` 📖	mathematical	`Polynomial.IsPrimitive` `CommRing.toCommSemiring`	`Polynomial.primPart`	—	`one_mul` `Polynomial.C_1` `content_eq_one` `Polynomial.eq_C_content_mul_primPart`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimitive` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring`	`Polynomial.IsPrimitive`	—	`IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `Polynomial.coeff_C_mul`

---

← Back to Index