Theorems · Theorem · commutative algebra

Algebra.Extension.Cotangent.mk_C_mem_ker_cotangentComplex

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {σ : Type u_1}
  (G : Algebra.Generators R S σ) {r : R} (hr : MvPolynomial.C r ∈ G.ker),
  Algebra.Extension.Cotangent.mk ⟨MvPolynomial.C r, hr⟩ ∈ G.toExtension.cotangentComplex.ker

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra