Theorems · Theorem · commutative algebra
Derivation.eqOn_adjoin
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
{D1 D2 : Derivation R A M} {s : Set A}, Set.EqOn (⇑D1) (⇑D2) s → Set.EqOn ⇑D1 ⇑D2 ↑(Algebra.adjoin R s)- Defined in
- Mathlib.RingTheory.Derivation.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Setstatement and proof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- SetLike.coestatement and proof · cited by 8,199
- Subalgebrastatement · cited by 1,353
- map_addproof · cited by 964
- Set.EqOnstatement and proof · cited by 603
- Algebra.adjoinstatement and proof · cited by 535
- Derivationstatement and proof · cited by 293
Cited by3
Results whose statement or proof uses this declaration.
- Polynomial.derivation_extproof · cited by 2
- MvPolynomial.derivation_eqOn_supportedproof · cited by 1
- Derivation.ext_of_adjoin_eq_topproof · cited by 0