Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.finite.exists_fin

Modification history

2021-04-25 15:13

src/ring_theory/finiteness.lean

feat(ring_theory): fg_iff_exists_fin_generating_fam (#7343)

Added module.finite.exists_fin View on Github →