Theorems · Inductive type · commutative algebra

DividedPowerAlgebra.Rel

(R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [Module R M] → MvPolynomial (ℕ × M) R → MvPolynomial (ℕ × M) R → Prop

The type coding the basic relations that will give rise to the divided power algebra. The class of MvPolynomial.X (n, a) will be equal to dpow n a, for a ∈ M.

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

CommSemiringAddCommMonoidModule