Theorems · Theorem · commutative algebra
KaehlerDifferential.polynomialEquiv_comp_D
∀ (R : Type u) [inst : CommRing R], (KaehlerDifferential.polynomialEquiv R).compDer (KaehlerDifferential.D R (Polynomial R)) = Polynomial.derivative'
- Defined in
- Mathlib.RingTheory.Kaehler.Polynomial
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Polynomialstatement · cited by 5,681
- LinearEquivstatement · cited by 3,317
- Derivationstatement · cited by 293
- KaehlerDifferentialstatement · cited by 204
- KaehlerDifferential.Dstatement · cited by 92
- Polynomial.derivative'statement and proof · cited by 7
- Derivation.liftKaehlerDifferential_compproof · cited by 6
- LinearEquiv.compDerstatement · cited by 3
- KaehlerDifferential.polynomialEquivstatement · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- KaehlerDifferential.polynomialEquiv_Dproof · cited by 0