Theorems · Theorem · commutative algebra

Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [IsDomain R] [inst_5 : NormalizedGCDMonoid R] {p : Polynomial K},
  p ≠ 0 → IsUnit (IsLocalization.integerNormalization (nonZeroDivisors R) p).primPart → IsUnit p

Defined in: Mathlib.RingTheory.Polynomial.GaussLemma
Cited by: 1 results in Mathlib
Foundations: Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Field Algebra IsFractionRing IsDomain NormalizedGCDMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites34

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapproof · cited by 4,706
Unitsproof · cited by 2,804
IsDomainstatement and proof · cited by 2,196
Units.valproof · cited by 1,966
IsUnitstatement and proof · cited by 1,602
Polynomial.Cproof · cited by 1,598
map_mulproof · cited by 1,137

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_mapproof · cited by 4