GaussLemma

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

Statistics

Metric	Count
Definitions	0
Theorems eq_map_mul_C_of_dvd, dvd_iff_map_cast_dvd_map_cast, irreducible_iff_irreducible_map_cast, dvd_iff_fraction_map_dvd_fraction_map, dvd_of_fraction_map_dvd_fraction_map, irreducible_iff_irreducible_map_fraction_map, irreducible_of_irreducible_map_of_injective, isUnit_iff_isUnit_map, isUnit_iff_isUnit_map_of_injective, dvd_iff_fraction_map_dvd_fraction_map, dvd_of_fraction_map_dvd_fraction_map, irreducible_iff_irreducible_map_fraction_map, isIntegrallyClosed_iff', isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart, mem_lifts_of_monic_of_dvd_map	15
Total	15

IsIntegrallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_map_mul_C_of_dvd 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.leadingCoeff	—	ne_zero_of_dvd_ne_zero Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.Monic.map Associated.dvd_iff_dvd_left associated_mul_isUnit_left_iff Polynomial.isUnit_C Ne.isUnit inv_ne_zero Polynomial.leadingCoeff_ne_zero Associated.refl integralClosure_eq_bot IsFractionRing.injective RingHom.ext AlgEquiv.symm_apply_apply Polynomial.mem_lifts integralClosure.mem_lifts_of_monic_of_dvd_map Polynomial.monic_mul_leadingCoeff_inv Polynomial.map_map mul_assoc Polynomial.C_mul inv_mul_cancel₀ Polynomial.C_1 mul_one

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegrallyClosed_iff' 📖	mathematical	—	IsIntegrallyClosed Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map algebraMap	—	Monic.irreducible_iff_irreducible_map_fraction_map isIntegrallyClosed_iff RingHom.mem_range minpoly.mem_range_of_degree_eq_one Monic.degree_map IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.monic degree_eq_one_of_irreducible_of_root instIsDomain minpoly.irreducible IsRoot.eq_1 eval_map_algebraMap minpoly.aeval
isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart 📖	mathematical	IsUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring primPart IsLocalization.integerNormalization nonZeroDivisors EuclideanDomain.toCommRing Field.toEuclideanDomain	DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	isUnit_iff IsDomain.to_noZeroDivisors IsLocalization.integerNormalization_map_to_map isUnit_of_mul_isUnit_right instIsDedekindFiniteMonoid algebraMap_apply Algebra.smul_def eq_C_content_mul_primPart map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass instIsDomain isUnit_iff_ne_zero injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass IsFractionRing.injective IsFractionRing.integerNormalization_eq_zero_iff content_eq_zero_iff mul_eq_zero Units.ne_zero IsDomain.toNontrivial map_mul map_C

Polynomial.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff_fraction_map_dvd_fraction_map 📖	mathematical	Polynomial.IsPrimitive CommRing.toCommSemiring	Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	—	Polynomial.map_mul dvd_of_fraction_map_dvd_fraction_map
dvd_of_fraction_map_dvd_fraction_map 📖	—	Polynomial.IsPrimitive CommRing.toCommSemiring Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map CommSemiring.toSemiring algebraMap	—	—	IsLocalization.integerNormalization_map_to_map Polynomial.map_injective IsFractionRing.injective Polynomial.map_mul Polynomial.algebraMap_apply Algebra.smul_def mul_assoc mul_comm Polynomial.map_C Associated.dvd_iff_dvd_right Associated.symm Polynomial.isUnit_primPart_C primPart_eq Polynomial.primPart_mul mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors ne_zero IsDomain.toNontrivial Polynomial.C_eq_zero Mathlib.Tactic.Contrapose.contrapose₃ dvd_primPart_iff_dvd
irreducible_iff_irreducible_map_fraction_map 📖	mathematical	Polynomial.IsPrimitive CommRing.toCommSemiring	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map algebraMap	—	Irreducible.not_isUnit isUnit_iff_isUnit_map IsLocalization.integerNormalization_map_to_map mul_ne_zero IsDomain.to_noZeroDivisors mem_nonZeroDivisors_iff_ne_zero IsDomain.toNontrivial Polynomial.map_injective IsFractionRing.injective Polynomial.map_mul Polynomial.algebraMap_apply Algebra.smul_def Polynomial.map_C 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 dvd_dvd_iff_associated IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero normalize_eq_normalize_iff MonoidWithZeroHom.map_mul Polynomial.normalize_content mul_one content_eq_one Polynomial.content_C Polynomial.content_mul mul_eq_zero Polynomial.instNoZeroDivisors instIsDomain ne_zero Polynomial.map_zero Irreducible.isUnit_or_isUnit mul_left_cancel₀ Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd Polynomial.C_eq_zero mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_comm Polynomial.eq_C_content_mul_primPart Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart isUnit_of_mul_isUnit_right instIsDedekindFiniteMonoid irreducible_of_irreducible_map_of_injective
irreducible_of_irreducible_map_of_injective 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Polynomial.IsPrimitive Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map	—	—	Irreducible.not_isUnit IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_iff_isUnit_map_of_injective Polynomial.isPrimitive_of_dvd Dvd.intro Dvd.intro_left Irreducible.isUnit_or_isUnit Polynomial.map_mul
isUnit_iff_isUnit_map 📖	mathematical	Polynomial.IsPrimitive CommRing.toCommSemiring	IsUnit Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map algebraMap	—	isUnit_iff_isUnit_map_of_injective instIsDomain IsFractionRing.injective
isUnit_iff_isUnit_map_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Polynomial.IsPrimitive	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map	—	RingHom.isUnit_map Polynomial.isUnit_iff IsDomain.to_noZeroDivisors Polynomial.degree_C Units.ne_zero IsDomain.toNontrivial Polynomial.eq_C_of_degree_eq_zero Polynomial.degree_map_eq_of_injective Polynomial.isUnit_C Polynomial.isPrimitive_iff_isUnit_of_C_dvd dvd_rfl

Polynomial.IsPrimitive.Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff_map_cast_dvd_map_cast 📖	mathematical	Polynomial.IsPrimitive Int.instCommSemiring	Polynomial Int.instSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Int.instCommRing Rat.semiring Rat.commRing Polynomial.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map Rat.isFractionRing Int.instIsDomain instNonemptyNormalizedGCDMonoid
irreducible_iff_irreducible_map_cast 📖	mathematical	Polynomial.IsPrimitive Int.instCommSemiring	Irreducible Polynomial Int.instSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Rat.semiring Polynomial.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Rat.commRing	—	Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map Rat.isFractionRing Int.instIsDomain instNonemptyNormalizedGCDMonoid

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff_fraction_map_dvd_fraction_map 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	—	dvd_of_fraction_map_dvd_fraction_map Polynomial.map_mul
dvd_of_fraction_map_dvd_fraction_map 📖	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	—	—	IsIntegrallyClosed.eq_map_mul_C_of_dvd dvd_of_mul_left_eq dvd_of_mul_right_eq Polynomial.map_injective IsFractionRing.injective Polynomial.map_mul mul_one Polynomial.C_1 leadingCoeff of_mul_monic_left map
irreducible_iff_irreducible_map_fraction_map 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map algebraMap	—	irreducible_iff Irreducible.not_isUnit Polynomial.IsPrimitive.isUnit_iff_isUnit_map isPrimitive IsIntegrallyClosed.eq_map_mul_C_of_dvd dvd_of_mul_right_eq dvd_of_mul_left_eq Polynomial.leadingCoeff_mul IsDomain.to_noZeroDivisors instIsDomain leadingCoeff map Polynomial.coe_mapRingHom IsUnit.mul IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Irreducible.isUnit_or_isUnit Polynomial.map_injective IsFractionRing.injective Polynomial.map_mul one_mul Polynomial.C_1 Polynomial.C_mul mul_assoc mul_comm isUnit_iff_exists_inv instIsDedekindFiniteMonoid isUnit_iff_exists_inv' Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_lifts_of_monic_of_dvd_map 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	Subsemiring Semiring.toNonAssocSemiring Polynomial.semiring SetLike.instMembership Subsemiring.instSetLike Polynomial.lifts Subalgebra Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring Semifield.toCommSemiring Subalgebra.toAlgebra Algebra.id	—	Polynomial.Splits.mem_lift_of_roots_mem_range instIsDomain Polynomial.SplittingField.splits Polynomial.Monic.map SetLike.ext_iff Subalgebra.range_algebraMap roots_mem_integralClosure Polynomial.aroots_def IsScalarTower.algebraMap_eq Polynomial.map_map Multiset.mem_of_le Polynomial.roots.le_of_dvd Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.map_dvd Polynomial.lifts_iff_coeff_lifts RingHom.coe_range SetLike.mem_coe Polynomial.eval₂_eq_eval_map injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass RingHom.injective DivisionRing.isSimpleRing Polynomial.eval₂_at_apply Polynomial.eval₂_map Polynomial.coeff_map

---

← Back to Index