mathlib

9acc1d40 - feat(model_theory/finitely_generated): Finitely generated and countably generated (sub)structures (#11857)

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