Theorems · Definition · commutative algebra

KaehlerDifferential.mulActionBaseChange

(R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [inst_3 : CommRing A] → [inst_4 : Algebra R A] → MulAction A (TensorProduct R S Ω[A⁄R])

(Implementation). A-action on S ⊗[R] Ω[A⁄R].

Defined in

Mathlib.RingTheory.Kaehler.TensorProduct

Cited by

3 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebra