Theorems · Definition · commutative algebra
Algebra.Generators.self
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S S
The Generators containing the whole algebra, which induces the canonical map R[S] → S.
- Defined in
- Mathlib.RingTheory.Extension.Generators
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- MvPolynomial.Xproof · cited by 552
- AlgHom.toRingHomproof · cited by 490
- RingHom.toAlgebraproof · cited by 337
- MvPolynomial.aevalproof · cited by 298
- Algebra.Generatorsstatement · cited by 152
Cited by33
Results whose statement or proof uses this declaration.
- Algebra.H1Cotangentproof · cited by 27
- Algebra.H1Cotangent.mapstatement and proof · cited by 11
- Algebra.FormallySmooth.comp_surjectiveproof · cited by 6
- Algebra.FormallySmooth.of_comp_surjectiveproof · cited by 6
- Algebra.H1Cotangent.δstatement and proof · cited by 4
- Algebra.Extension.defaultHomstatement · cited by 4
- Algebra.Extension.h1CotangentEquivCotangentstatement · cited by 3
- Algebra.Extension.h1CotangentExtendScalarsEquivstatement and proof · cited by 3
- Algebra.etaleLocus_eq_compl_supportstatement · cited by 2
- Algebra.smoothLocus_eq_compl_support_interstatement · cited by 2
- Algebra.tensorH1CotangentOfFlatstatement and proof · cited by 2
- Algebra.tensorH1CotangentOfIsLocalizationstatement and proof · cited by 2