Theorems · Definition · commutative algebra
Algebra.Presentation.differentialsSolution
{R : Type u} →
{S : Type v} →
{ι : Type w} →
{σ : Type t} →
[inst : CommRing R] →
[inst_1 : CommRing S] →
[inst_2 : Algebra R S] → (pres : Algebra.Presentation R S ι σ) → pres.differentialsRelations.Solution Ω[S⁄R]The S-module Ω[S⁄R] contains an obvious solution to the system of linear
equations pres.differentialsRelations.Solution when pres is a presentation
of S as an R-algebra.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- KaehlerDifferentialstatement · cited by 204
- Algebra.Generators.valproof · cited by 115
- Algebra.Presentation.toGeneratorsproof · cited by 104
- Module.Relations.Gproof · cited by 103
- KaehlerDifferential.Dproof · cited by 92
- Module.Relations.Solutionstatement · cited by 70
- Algebra.Presentationstatement and proof · cited by 70
- Module.Relations.Rproof · cited by 57
- Algebra.Presentation.differentialsRelationsstatement and proof · cited by 6
Cited by3
Results whose statement or proof uses this declaration.
- Algebra.Presentation.differentials.comm₂₃statement · cited by 1
- Algebra.Presentation.differentialsSolution_isPresentationstatement and proof · cited by 0
- Algebra.Presentation.differentialsproof · cited by 0