Theorems · Theorem · field theory
Polynomial.Sequence.span
∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R),
(∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) → Submodule.span R (Set.range ↑S) = ⊤A polynomial sequence spans R[X] if all of its elements' leading coefficients are units.
- Defined in
- Mathlib.Algebra.Polynomial.Sequence
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- Polynomialstatement and proof · cited by 5,681
- Set.imageproof · cited by 5,609
- Set.rangestatement and proof · cited by 4,705
- IsUnitstatement and proof · cited by 1,602
- Submodule.spanstatement and proof · cited by 1,504
- Set.Iioproof · cited by 1,166
- Polynomial.natDegreeproof · cited by 1,105
- Polynomial.leadingCoeffstatement and proof · cited by 498
- Submodule.span_monoproof · cited by 85
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.