Theorems · Theorem · commutative algebra
RingHom.isIntegralElem_leadingCoeff_mul
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R) (x : S),
Polynomial.eval₂ f x p = 0 → f.IsIntegralElem (f p.leadingCoeff * x)Given a p : R[X] and a x : S such that p.eval₂ f x = 0,
f p.leadingCoeff * x is integral.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Semiringproof · cited by 13,802
- RingHomstatement and proof · cited by 10,189
- Polynomialstatement and proof · cited by 5,681
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
- Polynomial.Cproof · cited by 1,598
- Polynomial.natDegreeproof · cited by 1,105
- Polynomial.coeffproof · cited by 1,045
- Polynomial.mapproof · cited by 806
- Polynomial.leadingCoeffstatement and proof · cited by 498
Cited by2
Results whose statement or proof uses this declaration.
- isIntegral_leadingCoeff_smulproof · cited by 2
- IsLocalization.exists_isIntegral_smul_of_isIntegral_mapproof · cited by 2