mathlib3
5d8b4328
- feat(model_theory/language_map): Cardinality of languages with constants (#13981)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(model_theory/language_map): Cardinality of languages with constants (#13981) `first_order.language.card_with_constants` shows that the cardinality of `L[[A]]` is `L.card + # A`.
Author
awainverse
Parents
4eb76a7b
Loading