Commit 2023-09-20 00:51 f1e1b398

View on Github →

feat(ModelTheory): The theory of fields of charP (#7188)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Algebra/Field/CharP.lean

added theorem FirstOrder.Field.charP_iff_model_fieldOfChar

added theorem FirstOrder.Field.charP_of_model_fieldOfChar

added theorem FirstOrder.Field.realize_eqZero

added def FirstOrder.Language.Theory.fieldOfChar