Theorems · Inductive type · ring theory
Subalgebra
(R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Type v
A subalgebra is a sub(semi)ring that includes the range of algebraMap.
- Defined in
- Mathlib.Algebra.Algebra.Subalgebra.Basic
- Cited by
- 1,353 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- Algebrastatement · cited by 11,388
- CommSemiringstatement · cited by 10,911
Cited by1,578
Results whose statement or proof uses this declaration.
- Algebra.adjoinstatement · cited by 535
- AlgHom.rangestatement · cited by 169
- Subalgebra.toSubmodulestatement and proof · cited by 141
- IntermediateField.toSubalgebrastatement · cited by 134
- Subalgebra.toSubsemiringstatement and proof · cited by 115
- Algebra.subset_adjoinstatement · cited by 109
- integralClosurestatement · cited by 105
- Subalgebra.valstatement and proof · cited by 104
- Subalgebra.mapstatement and proof · cited by 90
- Subalgebra.LinearDisjointstatement and proof · cited by 75
- IntermediateField.restrictScalarsproof · cited by 66
- IntermediateField.mapproof · cited by 62
Showing the 200 most cited of 1,578.