Theorems · Theorem · commutative algebra

MvPolynomial.killCompl_monomial_mapDomain

∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {s : σ →₀ ℕ} {c : R},
  (MvPolynomial.killCompl hf) ((MvPolynomial.monomial (Finsupp.mapDomain f s)) c) = (MvPolynomial.monomial s) c

Defined in: Mathlib.Algebra.MvPolynomial.Rename
Cited by: 1 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

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.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
Finsuppstatement and proof · cited by 5,255
AlgHomstatement · cited by 3,236
MvPolynomialstatement · cited by 2,140
MvPolynomial.monomialstatement and proof · cited by 253
Finsupp.mapDomainstatement · cited by 168
MvPolynomial.killComplstatement and proof · cited by 15
MvPolynomial.killCompl_rename_appproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subsetproof · cited by 1