Commit 2026-01-21 15:00 f99d0863

View on Github →

chore(ModelTheory): adjust precedence of [[.]] to max (#34210) Per suggestion by fpvandoorn in PR #33481. Most parentheses of expanded languages are removed now.

Estimated changes

Modified Mathlib/ModelTheory/Definability.lean

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/ModelTheory/LanguageMap.lean

Modified Mathlib/ModelTheory/Satisfiability.lean

Modified Mathlib/ModelTheory/Substructures.lean

modified theorem FirstOrder.Language.Substructure.subset_closure_withConstants

Modified Mathlib/ModelTheory/Topology/Types.lean

Modified Mathlib/ModelTheory/Types.lean

modified theorem FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem