Commit 2024-03-04 10:09 e612a999

View on Github →

chore(ModelTheory/DirectLimit): Fintype -> Finite, Encodable -> Countable (#10913)

Estimated changes

Modified Mathlib/ModelTheory/DirectLimit.lean

modified theorem FirstOrder.Language.DirectLimit.cg

modified theorem FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq

modified theorem FirstOrder.Language.DirectLimit.exists_unify_eq