Theorems · Theorem · commutative algebra

KaehlerDifferential.mvPolynomialBasis_repr_comp_D

∀ (R : Type u) [inst : CommRing R] (σ : Type u_1),
  (↑(KaehlerDifferential.mvPolynomialBasis R σ).repr).compDer (KaehlerDifferential.D R (MvPolynomial σ R)) =
    MvPolynomial.mkDerivation R fun x => fun₀ | x => 1

Defined in: Mathlib.RingTheory.Kaehler.Polynomial
Cited by: 1 results in Mathlib
Foundations: Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites16

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

DFunLike.coestatement · cited by 62,936
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
LinearMapstatement · cited by 10,215
Finsuppstatement · cited by 5,255
MvPolynomialstatement · cited by 2,140
LinearEquiv.toLinearMapstatement · cited by 1,171
Finsupp.singlestatement and proof · cited by 943
Module.Basis.reprstatement · cited by 498
Derivationstatement · cited by 293
KaehlerDifferentialstatement · cited by 204
KaehlerDifferential.Dstatement · cited by 92

Cited by1

Results whose statement or proof uses this declaration.

KaehlerDifferential.mvPolynomialBasis_repr_Dproof · cited by 1