Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 15:52 9acc1d40

View on Github →

feat(model_theory/finitely_generated): Finitely generated and countably generated (sub)structures (#11857) Defines substructure.fg and Structure.fg to indicate when (sub)structures are finitely generated Defines substructure.cg and Structure.cg to indicate when (sub)structures are countably generated

Estimated changes