Mathlib Map

Theorems · Definition · commutative algebra

Ideal.Cotangent

{R : Type u} → [inst : CommRing R] → Ideal R → Type u

I ⧸ I ^ 2 as a quotient of I.

Defined in
Mathlib.RingTheory.Ideal.Cotangent
Cited by
68 results in Mathlib
Foundations
Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

KaehlerDifferential · cited by 204KaehlerDifferentialAlgebra.Extension.Cotangent · cited by 121Extension.CotangentIdeal.toCotangent · cited by 45Ideal.toCotangentAlgebra.Extension.Cotangent.val · cited by 29Cotangent.valIsLocalRing.CotangentSpace · cited by 16IsLocalRing.CotangentSpaceIdeal.toCotangent_surjective · cited by 15Ideal.toCotangent_surject…Algebra.Extension.Cotangent.ext · cited by 15Cotangent.extKaehlerDifferential.kerCotangentToTensor · cited by 9KaehlerDifferential.kerCo…Ideal.cotangentToQuotientSquare · cited by 7Ideal.cotangentToQuotient…Ideal.mapCotangent · cited by 6Ideal.mapCotangentAlgebra.FormallySmooth.comp_surjective · cited by 6FormallySmooth.comp_surje…Algebra.Extension.H1Cotangent.map_eq · cited by 6H1Cotangent.map_eqAlgebra.Generators.Cotangent.exact · cited by 6Cotangent.exactAlgebra.Extension.Cotangent.of · cited by 5Cotangent.ofAlgebra.FormallySmooth.iff_split_surjection · cited by 5FormallySmooth.iff_split_…CommRing · cited by 17173CommRingTop.top · cited by 9680Top.topIdeal · cited by 4748IdealHasQuotient.Quotient · cited by 2301HasQuotient.QuotientIdeal.CotangentCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by84

Results whose statement or proof uses this declaration.