Theorems · Definition · commutative algebra

Algebra.Generators.naive

{R : Type u} →
  [inst : CommRing R] →
    {σ : Type u_2} →
      {I : Ideal (MvPolynomial σ R)} →
        (s : optParam (MvPolynomial σ R ⧸ I → MvPolynomial σ R) (Function.surjInv ⋯)) →
          autoParam (∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x) Algebra.Generators.naive._auto_1 →
            Algebra.Generators R (MvPolynomial σ R ⧸ I) σ

The naive generators for a quotient R[Xᵢ] ⧸ I. If the definitional equality of the section matters, it can be explicitly provided.

Defined in

Mathlib.RingTheory.Extension.Generators

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRing