Documentation

Mathlib.RingTheory.LocalRing.Quotient

We gather results about the quotients of local rings.

noncomputable def LocalRing.basisQuotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [LocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) :

Given a basis of S, the induced basis of S / Ideal.map (algebraMap R S) p.

Equations
Instances For
    theorem LocalRing.basisQuotient_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [LocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) (i : ι) :
    theorem LocalRing.basisQuotient_repr {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [LocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_4} [Fintype ι] (b : Basis ι R S) (x : S) (i : ι) :