Theorems · Theorem · commutative algebra
Module.Finite.fg_top
∀ {R : Type u_1} {M : Type u_4} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
[self : Module.Finite R M], ⊤.FGA module over a semiring is Module.Finite if it is finitely generated as a module.
- Defined in
- Mathlib.RingTheory.Finiteness.Defs
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Module.Finite
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.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Top.topstatement · cited by 9,680
- Submodulestatement · cited by 7,192
- Module.Finitestatement and proof · cited by 1,032
- Submodule.FGstatement · cited by 230
Cited by28
Results whose statement or proof uses this declaration.
- Module.finite_defproof · cited by 16
- Module.Finite.exists_fin'proof · cited by 10
- Module.FinitePresentation.fg_kerproof · cited by 6
- Submodule.top_ne_ideal_smul_of_le_jacobson_annihilatorproof · cited by 6
- Module.Finite.exists_finproof · cited by 5
- RingHom.Finite.to_isIntegralproof · cited by 3
- Module.Finite.of_isLocalized_maximalproof · cited by 2
- Module.Finite.of_localizationSpan_finite'proof · cited by 2
- TensorProduct.spanFinrank_top_eq_of_residueFieldproof · cited by 1
- Localization.localRingHom_surjective_of_primesOver_eq_singletonproof · cited by 1
- Localization.finite_of_primesOver_eq_singletonproof · cited by 1