Mathlib Map

Theorems · Definition · ring theory

SkewPolynomial.C

{R : Type u_1} → [inst : Semiring R] → R →+ SkewPolynomial R

C a is the constant SkewPolynomial a. C is provided as an additive homomorphism.

Defined in
Mathlib.Algebra.SkewPolynomial.Basic
Cited by
32 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Semiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SkewPolynomial.C_mul_X_pow_eq_monomial · cited by 3SkewPolynomial.C_mul_X_po…SkewPolynomial.coeff_C · cited by 3SkewPolynomial.coeff_CSkewPolynomial.C_0 · cited by 2SkewPolynomial.C_0SkewPolynomial.C_mul_X_eq_monomial · cited by 2SkewPolynomial.C_mul_X_eq…SkewPolynomial.support_C_mul_X_pow_subset · cited by 2SkewPolynomial.support_C_…SkewPolynomial.C_1 · cited by 1SkewPolynomial.C_1SkewPolynomial.C_inj · cited by 1SkewPolynomial.C_injSkewPolynomial.coeff_C_zero · cited by 1SkewPolynomial.coeff_C_ze…SkewPolynomial.CRingHom_eq_C · cited by 0SkewPolynomial.CRingHom_e…SkewPolynomial.C_add · cited by 0SkewPolynomial.C_addSkewPolynomial.C_eq_intCast · cited by 0SkewPolynomial.C_eq_intCa…SkewPolynomial.C_eq_natCast · cited by 0SkewPolynomial.C_eq_natCa…SkewPolynomial.C_eq_zero · cited by 0SkewPolynomial.C_eq_zeroSkewPolynomial.C_injective · cited by 0SkewPolynomial.C_injectiveSkewPolynomial.C_mul · cited by 0SkewPolynomial.C_mulSemiring · cited by 13802SemiringAddMonoidHom · cited by 3230AddMonoidHomMultiplicative · cited by 875MultiplicativeSkewPolynomial · cited by 124SkewPolynomialSkewMonoidAlgebra.singleAddHom · cited by 4SkewMonoidAlgebra.singleA…SkewPolynomial.CCITED BYCITES

Cites5

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

Cited by32

Results whose statement or proof uses this declaration.