Theorems · Definition · commutative algebra
RingHom.Finite
{A : Type u_1} → {B : Type u_2} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → PropA ring morphism A →+* B is RingHom.Finite if B is finitely generated as A-module.
- Defined in
- Mathlib.RingTheory.Finiteness.Defs
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
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.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- Module.Finiteproof · cited by 1,032
Cited by51
Results whose statement or proof uses this declaration.
- AlgHom.Finiteproof · cited by 11
- RingHom.Finite.of_surjectivestatement · cited by 8
- RingHom.Finite.compstatement and proof · cited by 7
- AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrankstatement and proof · cited by 6
- RingEquiv.finitestatement · cited by 5
- RingHom.IsIntegral.to_finitestatement · cited by 4
- RingHom.Finite.idstatement · cited by 3
- RingHom.Finite.to_isIntegralstatement and proof · cited by 3
- RingHom.finite_algebraMapstatement · cited by 3
- RingHom.finite_respectsIsostatement · cited by 3
- RingHom.QuasiFinite.of_finitestatement and proof · cited by 2
- RingHom.Finite.finiteTypestatement and proof · cited by 2