Theorems · Definition · commutative algebra

PolynomialModule.lsingle

(R : Type u_2) →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ℕ → M →ₗ[R] PolynomialModule R M

PolynomialModule.single as a linear map.

Defined in: Mathlib.Algebra.Polynomial.Module.Basic
Cited by: 12 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
LinearMapstatement · cited by 10,215
LinearMap.compproof · cited by 1,642
LinearEquiv.symmproof · cited by 1,461
LinearEquiv.toLinearMapproof · cited by 1,171
PolynomialModulestatement · cited by 76
Finsupp.lsingleproof · cited by 75
PolynomialModule.coeffLinearEquivproof · cited by 5

Cited by14

Results whose statement or proof uses this declaration.

PolynomialModule.compproof · cited by 6
taylor_within_zero_evalproof · cited by 6
PolynomialModule.comp_applystatement · cited by 3
PolynomialModule.comp_singleproof · cited by 1
PolynomialModule.eval_lsinglestatement · cited by 1
Ideal.Filtration.submodule_fg_iff_stableproof · cited by 1
PolynomialModule.hom_extstatement and proof · cited by 1
PolynomialModule.polynomialTensorProductLEquivPolynomialModuleproof · cited by 0
PolynomialModule.single_smulproof · cited by 0
PolynomialModule.comp_smulproof · cited by 0
PolynomialModule.hom_ext_iffstatement and proof · cited by 0
PolynomialModule.lsingle_applystatement · cited by 0