Theorems · Inductive type · commutative algebra
Algebra.FiniteType
(R : Type uR) → (A : Type uA) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
An algebra over a commutative semiring is of FiniteType if it is finitely generated
over the base ring as algebra.
- Defined in
- Mathlib.RingTheory.FiniteType
- Cited by
- 84 results in Mathlib
- Foundations
- Depth 2 from the axioms · 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 by93
Results whose statement or proof uses this declaration.
- RingHom.FiniteTypeproof · cited by 46
- Algebra.FiniteType.outstatement and proof · cited by 14
- Algebra.FiniteType.of_surjectivestatement and proof · cited by 11
- Algebra.FiniteType.iff_quotient_mvPolynomial''statement · cited by 10
- Algebra.FiniteType.isNoetherianRingstatement and proof · cited by 6
- isJacobsonRing_of_finiteTypestatement and proof · cited by 5
- RingHom.finiteType_algebraMapstatement and proof · cited by 5
- Algebra.IsIntegral.finitestatement and proof · cited by 5
- Algebra.FiniteType.casesOnstatement and proof · cited by 5
- finTrdeg_iff_trdegproof · cited by 4
- Algebra.QuasiFinite.iff_finite_comap_preimage_singletonstatement and proof · cited by 4
- finite_of_finite_type_of_isJacobsonRingstatement and proof · cited by 4