Theorem FirstOrder.Language.Term.realize_quotient_mk'

Modification history

2023-08-10 19:52

Mathlib/ModelTheory/Quotients.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified FirstOrder.Language.Term.realize_quotient_mk'View on Github →

2023-05-24 11:42

Mathlib/ModelTheory/Quotients.lean

feat: port ModelTheory.Quotients (#3972)

Added FirstOrder.Language.Term.realize_quotient_mk'View on Github →