Theorems · Definition · commutative algebra
Submodule.CoFG
{R : Type u_1} →
[inst : Ring R] → {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → PropA submodule S of a module M is co-finitely generated (CoFG) if the quotient
space M ⧸ S is finitely generated.
- Defined in
- Mathlib.RingTheory.Finiteness.Cofinite
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- HasQuotient.Quotientproof · cited by 2,301
- Module.Finiteproof · cited by 1,032
Cited by30
Results whose statement or proof uses this declaration.
- Submodule.CoFG.of_lestatement and proof · cited by 4
- Submodule.range_fg_iff_ker_cofgstatement and proof · cited by 2
- ContinuousLinearMap.isFredholm_iff_exists_isQuasiInverseproof · cited by 2
- ContinuousLinearMap.isFredholm_tfaestatement and proof · cited by 2
- LinearMap.FiniteRangeSetoid.equiv_iff_eqLocus_coFGstatement and proof · cited by 2
- ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrictstatement and proof · cited by 2
- LinearMap.ker_coFG_iff_hasFiniteRangestatement · cited by 2
- Submodule.CoFG.fg_of_disjointstatement and proof · cited by 1
- Submodule.CoFG.fg_of_isComplstatement and proof · cited by 1
- Submodule.CoFG.infstatement and proof · cited by 1
- Submodule.CoFG.kerstatement · cited by 1
- Submodule.CoFG.of_finitestatement · cited by 1