Theorems · Theorem · commutative algebra

Polynomial.IsPrimitive.mul_map_mem_lifts_iff

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {f : Polynomial R},
  f.IsPrimitive →
    ∀ {g : Polynomial K},
      g * Polynomial.map (algebraMap R K) f ∈ Polynomial.lifts (algebraMap R K) ↔ g ∈ Polynomial.lifts (algebraMap R K)

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites45

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

DFunLike.coeproof · cited by 62,936
Moduleproof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommMonoidproof · cited by 12,281
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapstatement and proof · cited by 4,706
mul_oneproof · cited by 3,885
IsDomainstatement and proof · cited by 2,196
Polynomial.Cproof · cited by 1,598
nonZeroDivisorsproof · cited by 895

Cited by2

Results whose statement or proof uses this declaration.

Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_mapproof · cited by 1
Polynomial.IsPrimitive.map_mul_mem_lifts_iffproof · cited by 0