Theorems · Definition · field theory
LaurentPolynomial.C
{R : Type u_1} → [inst : Semiring R] → R →+* LaurentPolynomial RThe ring homomorphism C, including R into the ring of Laurent polynomials over R as
the constant Laurent polynomials.
- Defined in
- Mathlib.Algebra.Polynomial.Laurent
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- RingHomstatement · cited by 10,189
- LaurentPolynomialstatement · cited by 98
- AddMonoidAlgebra.singleZeroRingHomproof · cited by 3
Cited by47
Results whose statement or proof uses this declaration.
- LaurentPolynomial.single_eq_C_mul_Tstatement · cited by 8
- Polynomial.toLaurent_Cstatement and proof · cited by 6
- Polynomial.toLaurent_C_mul_Tstatement and proof · cited by 4
- LaurentPolynomial.degree_C_mul_Tstatement and proof · cited by 4
- LaurentPolynomial.induction_on'statement and proof · cited by 4
- LaurentPolynomial.single_eq_Cstatement · cited by 4
- Polynomial.toLaurent_Xproof · cited by 3
- Matrix.reverse_charpolyproof · cited by 3
- LaurentPolynomial.support_coeff_C_mul_T_of_ne_zerostatement · cited by 2
- LaurentPolynomial.C_applystatement · cited by 2
- Polynomial.toLaurent_C_mul_eqstatement and proof · cited by 2
- LaurentPolynomial.degree_C_mul_T_lestatement and proof · cited by 2