Commit 2023-05-24 11:42 88a01cc3

View on Github →

feat: port ModelTheory.Quotients (#3972)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Quotients.lean

added theorem FirstOrder.Language.Term.realize_quotient_mk'

added theorem FirstOrder.Language.funMap_quotient_mk'

added theorem FirstOrder.Language.relMap_quotient_mk'