Theorems · Theorem · commutative algebra
Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R} (h_prin : Submodule.IsPrincipal p.contentIdeal) (n : ℕ),
Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n- Cited by
- 2 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement and proof · cited by 5,681
- Polynomial.coeffstatement and proof · cited by 1,045
- Submodule.IsPrincipalstatement and proof · cited by 129
- Submodule.IsPrincipal.generatorstatement and proof · cited by 56
- Polynomial.contentIdealstatement and proof · cited by 24
- Submodule.IsPrincipal.mem_iff_eq_smul_generatorproof · cited by 3
- Polynomial.coeff_mem_contentIdealproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- Submodule.IsPrincipal.contentIdeal_generator_dvdproof · cited by 2
- Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipalproof · cited by 0