Def FirstOrder.Language.Theory.fieldOfChar

Modification history

2026-07-24 07:15
Mathlib/ModelTheory/Algebra/Field/CharP.lean
chore: add missing `noncomputable` (#41446) …
Deleted FirstOrder.Language.Theory.fieldOfCharView on Github →
2023-09-20 00:51
Mathlib/ModelTheory/Algebra/Field/CharP.lean
feat(ModelTheory): The theory of fields of charP (#7188)
Added FirstOrder.Language.Theory.fieldOfCharView on Github →