Theorems · Theorem · commutative algebra
Submodule.fg_bot
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.FG- Defined in
- Mathlib.RingTheory.Finiteness.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Submodulestatement and proof · cited by 7,192
- Bot.botstatement and proof · cited by 4,720
- Submodule.spanproof · cited by 1,504
- Submodule.FGstatement · cited by 230
- Finset.coe_emptyproof · cited by 109
- Submodule.span_emptyproof · cited by 29
Cited by13
Results whose statement or proof uses this declaration.
- TensorProduct.exists_finite_submodule_of_setFiniteproof · cited by 3
- Submodule.exists_fg_le_eq_rTensor_subtypeproof · cited by 2
- RingHom.finitePresentation_respectsIsoproof · cited by 2
- Submodule.fg_finset_supproof · cited by 1
- FractionalIdeal.isNoetherian_zeroproof · cited by 1
- isNoetherian_iff_fg_wellFoundedproof · cited by 1
- Algebra.FinitePresentation.iff_quotient_mvPolynomial'proof · cited by 1
- RingHom.FinitePresentation.of_bijectiveproof · cited by 1
- IsNoetherianRing.of_prime_ne_botproof · cited by 0
- Localization.exists_awayMap_bijective_of_residueField_surjectiveproof · cited by 0
- Algebra.FinitePresentation.mvPolynomial_of_finitePresentationproof · cited by 0
- Submodule.fg_sup_span_inductionstatement and proof · cited by 0