Theorems · Inductive type · commutative algebra
Algebra.Generators
(R : Type u) → (S : Type v) → Type w → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max u v) w)
A family of generators of an R-algebra S consists of
1. ι: The type of variables.
2. val : ι → S: The assignment of each variable to a value in S.
3. σ: A section of R[X] → S.
- Defined in
- Mathlib.RingTheory.Extension.Generators
- Cited by
- 152 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 22 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by225
Results whose statement or proof uses this declaration.
- Algebra.Generators.Ringstatement and proof · cited by 133
- Algebra.Generators.valstatement and proof · cited by 115
- Algebra.Presentation.toGeneratorsstatement · cited by 104
- Algebra.Generators.toExtensionstatement and proof · cited by 103
- Algebra.Generators.compstatement and proof · cited by 52
- Algebra.Generators.kerstatement and proof · cited by 46
- Algebra.Generators.Hom.toExtensionHomstatement and proof · cited by 37
- Algebra.Generators.algebraMap_applystatement and proof · cited by 32
- Algebra.Generators.ofCompstatement and proof · cited by 32
- Algebra.Generators.Hom.toAlgHomstatement and proof · cited by 30
- Algebra.Generators.σstatement and proof · cited by 29
- Algebra.Generators.Homstatement · cited by 28
Showing the 200 most cited of 225.